Proof by consistency in conditional equational theories

DOI10.1007/3-540-54317-1_91MaRDI QIDQ5881278zbMATH OpenOpenAlexFDO

Authors Eddy Bevers, Johan Lewi

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_91

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Recommendations

• Proof by consistency
• Automatic proofs by induction in theories without constructors
• Inductive theorem proving by consistency for first-order clauses
• Induction = I-axiomatization + first-order consistency.
• Inductive proofs by specification transformations

Cites work

• A strong restriction of the inductive completion procedure
• Conditional rewrite rules
• scientific article; zbMATH DE number 3891336 (Why is no real title available?)
• scientific article; zbMATH DE number 3921957 (Why is no real title available?)
• scientific article; zbMATH DE number 3956434 (Why is no real title available?)
• scientific article; zbMATH DE number 4047063 (Why is no real title available?)
• scientific article; zbMATH DE number 4090780 (Why is no real title available?)
• scientific article; zbMATH DE number 4090848 (Why is no real title available?)
• scientific article; zbMATH DE number 4092758 (Why is no real title available?)
• scientific article; zbMATH DE number 4092821 (Why is no real title available?)
• scientific article; zbMATH DE number 3684925 (Why is no real title available?)
• Orderings for term-rewriting systems
• Semantic confluence tests and completion methods
• Simplifying conditional term rewriting systems: Unification, termination and confluence

Cited in

(21)

• Proof by consistency
• Soundness of abductive proof procedure with respect to constraint for non-ground abducibles
• The equational part of proofs by structural induction
• Extending Bachmair's method for proof by consistency to the final algebra
• A formalisation of consistent consequence for Boolean equation systems
• Induction = I-axiomatization + first-order consistency.
• Implicit induction in conditional theories
• An algebraic characterization of inductive soundness in proof by consistency
• Proof-irrelevant model of CC with predicative induction and judgmental equality
• Theorem proving for conditional logics: CondLean and GOALDUCK
• scientific article; zbMATH DE number 4090849 (Why is no real title available?)
• Equation solving in conditional AC-theories
• Induction using term orderings
• On the connection between narrowing and proof by consistency
• On notions of inductive validity for first-order equational clauses
• scientific article; zbMATH DE number 5235521 (Why is no real title available?)
• Inductive theorem proving by consistency for first-order clauses
• A calculus for conditional inductive theorem proving
• A general framework to build contextual cover set induction provers
• Higher-order proof by consistency
• Conditional equational theories and complete sets of transformations

This page was built for publication: Proof by consistency in conditional equational theories

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