Controlled use of clausal lemmas in connection tableau calculi

DOI10.1006/jsco.1999.0363zbMath0969.03018OpenAlexW2018015794WikidataQ124987221 ScholiaQ124987221MaRDI QIDQ5927985

Marc Fuchs

Publication date: 19 March 2001

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/92354a3350e26fef78dcd6588213a1efefcf0e66

zbMATH Keywords

clausal lemmastableaux

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies

Uses Software

• SETHEO
• TPTP
• E-SETHEO

Cites Work

• Depth-first iterative-deepening: An optimal admissible tree search
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• SETHEO: A high-performance theorem prover
• Refutation graphs
• Controlled integration of the cut rule into connection tableau calculi
• The use of lemmas in the model elimination procedure
• A disjunctive positive refinement of model elimination and its application to subsumption deletion
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Optimizing proof search in model elimination
• The TPTP problem library
• Integration of automated and interactive theorem proving in ILF
• Lemma matching for a PTTP-based top-down theorem prover
• Mechanical Theorem-Proving by Model Elimination
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item