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

DOI10.1016/0020-0190(94)00109-XzbMATH Open0822.68101OpenAlexW2066687655MaRDI QIDQ1336767FDOQ1336767

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

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

zbMATH Keywords

abstract data typesBachmair's method

Mathematics Subject Classification ID

Equational logic, Mal'tsev conditions (08B05)

Cites Work

• Title not available (Why is that?)
• On sufficient-completeness and related properties of term rewriting systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Larch shared language handbook
• Resolution of equations in algebraic structures. Volume II: Rewriting techniques
• Title not available (Why is that?)
• Observational implementations

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)