A strong restriction of the inductive completion procedure

DOI10.1016/S0747-7171(89)80069-0zbMath0682.68029MaRDI QIDQ1824381

Laurent Fribourg

Publication date: 1989

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

selection functioncompletion procedureKnuth-Bendix procedureground-confluenceprinciple of definition

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Related Items

Proof by consistency in conditional equational theories ⋮ Computing ground reducibility and inductively complete positions ⋮ Induction using term orders ⋮ Applying term rewriting methods to finite groups ⋮ Specification and proof in membership equational logic ⋮ Using induction and rewriting to verify and complete parameterized specifications ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ A general framework to build contextual cover set induction provers ⋮ Deductive and inductive synthesis of equational programs

Cites Work

• Conditional rewrite rules
• Inductive completion with retracts
• Mechanizing structural induction. II: Strategies
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Deductive synthesis of the unification algorithm
• Reasoning about programs
• Oriented equational clauses as a programming language
• Semantic confluence tests and completion methods
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Proving Properties of Programs by Structural Induction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item