Higher-order proof by consistency

DOI10.1007/3-540-62034-6_56MaRDI QIDQ6567778zbMATHFDO

Authors Henrik Linnestad, Christian Prehofer, Olav Lysne

Publication date 5 July 2024

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Induction = I-axiomatization + first-order consistency.
• Proof by consistency
• Inductive theorem proving by consistency for first-order clauses
• Proof by consistency in conditional equational theories
• Rewriting Techniques and Applications

Cites work

• scientific article; zbMATH DE number 3956434 (Why is no real title available?)
• scientific article; zbMATH DE number 3684925 (Why is no real title available?)
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 50648 (Why is no real title available?)
• scientific article; zbMATH DE number 1300969 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• A logic programming language with lambda-abstraction, function variables, and simple unification
• A termination ordering for higher order rewrite systems
• Decidable higher-order unification problems
• Extending Bachmair's method for proof by consistency to the final algebra
• Isabelle. A generic theorem prover
• On sufficient-completeness and related properties of term rewriting systems
• Proof by consistency in conditional equational theories
• Proofs by induction in equational theories with constructors
• Term rewriting induction
• Towards a domain theory for termination proofs

This page was built for publication: Higher-order proof by consistency

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