Controlled use of clausal lemmas in connection tableau calculi
From MaRDI portal
Publication:5927985
DOI10.1006/jsco.1999.0363zbMath0969.03018OpenAlexW2018015794WikidataQ124987221 ScholiaQ124987221MaRDI QIDQ5927985
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
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
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
