scientific article; zbMATH DE number 3827173

MaRDI QIDQ3673071zbMATH OpenFDO

Authors Jean-Pierre Jouannaud

Publication date 1983

zbMATH Keywords

algebraic specificationsChurch-Rosser propertycoherenceconfluenceconsistencycritical pairsdata typesequational deductionterm rewriting

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Word problems (aspects of algebraic structures) (08A50) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Symbolic computation and algebraic computation (68W30)

Cited in

(16)

• Parameter-preserving data type specifications
• Unification in varieties of idempotent semigroups
• History and basic features of the critical-pair/completion procedure
• Semantics of order-sorted specifications
• Completion for rewriting modulo a congruence
• On deciding confluence of finite string-rewriting systems modulo partial commutativity
• Invariants and closures in the theory of rewrite systems
• Conditional rewrite rule systems with built-in arithmetic and induction
• Unification properties of commutative theories: a categorical treatment
• Unification in commutative theories
• Theorem proving modulo associativity
• Strict coherence of conditional rewriting modulo axioms
• Confluence of conditional rewriting modulo
• Nominal equational rewriting and narrowing
• Nominal equational narrowing: rewriting for unification in languages with binders
• Equational completion in order-sorted algebras

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3673071)