Simplifying conditional term rewriting systems: Unification, termination and confluence
type: Item
instance of: scholarly article
title: Simplifying conditional term rewriting systems: Unification, termination and confluence
zbMATH Open document ID: 0641.68046
DOI: 10.1016/S0747-7171(87)80010-X
author: Stéphane Kaplan
published in: Journal of Symbolic Computation
publication date: 1987-01-01T00:00:00Z
review text: In the field of conditional term rewriting systems, the reduction of a given term involves recursive reduction of the premises of the rule currently applied, which leads to intractability. In this paper, we introduce simplifying systems, that allow to control this recursivity. Our approach enables the extension of several results for non-conditional rewriting to the conditional framework. In particular, we obtain results about the correctness of evaluation procedures, unification in conditional theories, termination and confluence, together with Knuth- Bendix theorem proving methods. Finally, the extension of such results to fully general conditional systems is discussed.
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 4045130
zbMATH Keywords: conditional term rewriting systems
zbMATH Keywords: recursivity
zbMATH Keywords: unification
zbMATH Keywords: termination
zbMATH Keywords: confluence
zbMATH Keywords: theorem proving
describes a project that uses: REVE
MaRDI profile type: Publication
cites work: Q3912001
cites work: Conditional rewrite rules: Confluence and termination
cites work: Algebraic specifications of computable and semicomputable data types
cites work: Q3894958
cites work: Q3703288
cites work: Q3210187
cites work: Q3696498
cites work: Q3347272
cites work: Q3731027
cites work: Q3336735
cites work: Q3880309
cites work: Proofs by induction in equational theories with constructors
cites work: Q3883561
cites work: Q3703312
cites work: Conditional rewrite rules
cites work: Q5581665
cites work: Computing in systems described by equations
cites work: Q3698310
cites work: Q3341872
cites work: Q3696486
description: scientific article; zbMATH DE number 4045130