A strong restriction of the inductive completion procedure

DOI10.1016/S0747-7171(89)80069-0MaRDI QIDQ1824381zbMATH OpenFDO

Authors Laurent Fribourg

Publication date 1989

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

Full work available at URL https://doi.org/10.1016/S0747-7171(89)80069-0

zbMATH Keywords

completion procedureground-confluenceKnuth-Bendix procedureprinciple of definitionselection function

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 3956434
• Completion procedures as semidecision procedures
• scientific article; zbMATH DE number 3891336
• scientific article; zbMATH DE number 44069
• Automatic proofs by induction in theories without constructors

Cites work

• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Conditional rewrite rules
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Deductive synthesis of the unification algorithm
• scientific article; zbMATH DE number 3870639 (Why is no real title available?)
• scientific article; zbMATH DE number 3930339 (Why is no real title available?)
• scientific article; zbMATH DE number 3938563 (Why is no real title available?)
• scientific article; zbMATH DE number 4043234 (Why is no real title available?)
• scientific article; zbMATH DE number 4047062 (Why is no real title available?)
• scientific article; zbMATH DE number 4047063 (Why is no real title available?)
• scientific article; zbMATH DE number 3684925 (Why is no real title available?)
• scientific article; zbMATH DE number 3688776 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Inductive completion with retracts
• Mechanizing structural induction. II: Strategies
• Oriented equational clauses as a programming language
• Proving Properties of Programs by Structural Induction
• Reasoning about programs
• Semantic confluence tests and completion methods

Cited in

(21)

• Inductive completion with retracts
• Deductive and inductive synthesis of equational programs
• Induction using term orders
• Specification and proof in membership equational logic
• Strong forward induction
• scientific article; zbMATH DE number 3891336 (Why is no real title available?)
• scientific article; zbMATH DE number 3956434 (Why is no real title available?)
• scientific article; zbMATH DE number 44069 (Why is no real title available?)
• Computing ground reducibility and inductively complete positions
• Proving equational and inductive theorems by completion and embedding techniques
• Applying term rewriting methods to finite groups
• Induction using term orderings
• Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation
• Proof by consistency in conditional equational theories
• Completion procedures as semidecision procedures
• A general framework to build contextual cover set induction provers
• The strength of sharply bounded induction requires MSP
• On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
• Using induction and rewriting to verify and complete parameterized specifications
• Towards a foundation of completion procedures as semidecision procedures
• A unified view of induction reasoning for first-order logic

This page was built for publication: A strong restriction of the inductive completion procedure

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