scientific article; zbMATH DE number 3827173

MaRDI QIDQ3673071zbMATH OpenFDO

Authors Jean-Pierre Jouannaud

Publication date 1983

zbMATH Keywords

coherenceconsistencyconfluenceterm rewritingalgebraic specificationsdata typesChurch-Rosser propertycritical pairsequational deduction

Mathematics Subject Classification ID

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

Cited in

(13)

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

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)