Building Theorem Provers

DOI10.1007/978-3-642-02959-2_24zbMath1250.68235OpenAlexW1762924921MaRDI QIDQ5191110

Mark E. Stickel

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_24

zbMATH Keywords

BCI logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Uses Software

• OTTER

Cites Work

• Logic-based subsumption architecture
• Connection tableaux with lazy paramodulation
• Depth-first iterative-deepening: An optimal admissible tree search
• Associative-commutative unification
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
• A Prolog technology theorem prover: A new exposition and implementation in Prolog
• Solution of the Robbins problem
• A fully syntactic AC-RPO.
• Automated deduction by theory resolution
• Z-Resolution: Theorem-Proving with Compiled Axioms
• A Unification Algorithm for Associative-Commutative Functions
• A Deductive Approach to Program Synthesis
• Complete Sets of Reductions for Some Equational Theories
• Term Rewriting and All That
• Automated Reasoning
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• Automated Deduction – CADE-19
• A milestone reached and a secret revealed
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Building Theorem Provers