Completion procedures as semidecision procedures

DOI10.1007/3-540-54317-1_92MaRDI QIDQ5881279zbMATH OpenOpenAlexFDO

Authors Maria Paola Bonacina, Jieh Hsiang

Publication date 9 March 2023

Published in Conditional and Typed Rewriting Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-54317-1_92

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Towards a foundation of completion procedures as semidecision procedures
• scientific article; zbMATH DE number 44069
• scientific article; zbMATH DE number 3956434
• A strong restriction of the inductive completion procedure
• On fairness of completion-based theorem proving strategies

Cites work

• scientific article; zbMATH DE number 4016226 (Why is no real title available?)
• scientific article; zbMATH DE number 3829296 (Why is no real title available?)
• scientific article; zbMATH DE number 4047063 (Why is no real title available?)
• scientific article; zbMATH DE number 4049135 (Why is no real title available?)
• scientific article; zbMATH DE number 4053061 (Why is no real title available?)
• scientific article; zbMATH DE number 4064978 (Why is no real title available?)
• scientific article; zbMATH DE number 4078851 (Why is no real title available?)
• scientific article; zbMATH DE number 3684925 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• A Unification Algorithm for Associative-Commutative Functions
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Automated proofs of the Moufang identities in alternative rings
• Complete Sets of Reductions for Some Equational Theories
• Completion of a Set of Rules Modulo a Set of Equations
• Computing with rewrite systems
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• On fairness of completion-based theorem proving strategies
• Proof by consistency
• Proofs by induction in equational theories with constructors
• Proving termination with multiset orderings
• Refutational theorem proving using term-rewriting systems
• Rewrite method for theorem proving in first order theory with equality
• Semantic confluence tests and completion methods
• Termination of rewriting

Cited in

(9)

• Semi-initial completions
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• On the modelling of search in theorem proving -- towards a theory of strategy analysis
• A rewriting approach to satisfiability procedures.
• Equational inference, canonical proofs, and proof orderings
• On proving properties of completion strategies
• scientific article; zbMATH DE number 3956434 (Why is no real title available?)
• Induction using term orderings
• A strong restriction of the inductive completion procedure

Describes a project that uses

Uses Software

• SbReve2

This page was built for publication: Completion procedures as semidecision procedures

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