Reasoning with conditional axioms

DOI10.1007/BF01534452zbMath0855.68097OpenAlexW1985483701WikidataQ114693866 ScholiaQ114693866MaRDI QIDQ1924731

Emmanuel Kounalis, Michaël Rusinowitch

Publication date: 14 January 1997

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01534452

zbMATH Keywords

Horn clausesautomatically proving theorems

Mathematics Subject Classification ID

Related Items (1)

Sound generalizations in mathematical induction

Uses Software

• LARCH

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Theorem-proving with resolution and superposition
• Proofs by induction in equational theories with constructors
• Termination of rewriting
• Simplifying conditional term rewriting systems: Unification, termination and confluence
• Mechanizing structural induction. I: Formal system
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Semantic confluence tests and completion methods
• Proving refutational completeness of theorem-proving strategies
• A Machine-Oriented Logic Based on the Resolution Principle
• The Concept of Demodulation in Theorem Proving
• Proving Properties of Programs by Structural Induction

This page was built for publication: Reasoning with conditional axioms