Extending Bachmair's method for proof by consistency to the final algebra

DOI10.1016/0020-0190(94)00109-XMaRDI QIDQ1336767zbMATH OpenOpenAlexFDO

Authors Olav Lysne

Publication date 18 October 1995

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(94)00109-x

zbMATH Keywords

abstract data typesBachmair's method

Mathematics Subject Classification ID

Equational logic, Mal'tsev conditions (08B05)

Recommendations

• Proof by consistency
• scientific article; zbMATH DE number 3945335
• Proof by consistency in conditional equational theories
• Automatic proofs by induction in theories without constructors
• Inductive theorem proving by consistency for first-order clauses

Cites work

• scientific article; zbMATH DE number 3945335 (Why is no real title available?)
• scientific article; zbMATH DE number 3956434 (Why is no real title available?)
• scientific article; zbMATH DE number 3723898 (Why is no real title available?)
• scientific article; zbMATH DE number 1300969 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• A Larch shared language handbook
• Observational implementations
• On sufficient-completeness and related properties of term rewriting systems
• Resolution of equations in algebraic structures. Volume II: Rewriting techniques

Cited in

(3)

• Higher-order proof by consistency
• Proof by consistency
• Observational proofs by rewriting.

This page was built for publication: Extending Bachmair's method for proof by consistency to the final algebra

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