Controlled integration of the cut rule into connection tableau calculi

DOI10.1007/BF00881947zbMath0816.03005OpenAlexW2025252200MaRDI QIDQ1344875

V. Pereyra

Publication date: 22 February 1995

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

automated deductionatomic cutconnection tableau calculi

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)

Related Items (35)

Controlled integration of the cut rule into connection tableau calculi ⋮ \textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ The model evolution calculus as a first-order DPLL method ⋮ The disconnection tableau calculus ⋮ ILF-SETHEO ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Craig interpolation with clausal first-order tableaux ⋮ Clause trees: A tool for understanding and implementing resolution in automated reasoning ⋮ Computing answers with model elimination ⋮ IeanCOP: lean connection-based theorem proving ⋮ Subsumption-linear Q-resolution for QBF theorem proving ⋮ MGTP: A model generation theorem prover — Its advanced features and applications — ⋮ Non-elementary speed-ups in proof length by different variants of classical analytic calculi ⋮ Subgoal alternation in model elimination ⋮ A framework for using knowledge in tableau proofs ⋮ Resolution remains hard under equivalence ⋮ Complexity analysis of propositional resolution with autarky pruning ⋮ leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ Another look at graph coloring via propositional satisfiability ⋮ The disconnection method ⋮ Minimal model generation with positive unit hyper-resolution tableaux ⋮ Situational Calculus, linear connection proofs and STRIPS-like planning: An experimental comparison ⋮ The tableau-based theorem prover 3 T A P Version 4.0 ⋮ Optimizing proof search in model elimination ⋮ On the practical value of different definitional translations to normal form ⋮ Controlled use of clausal lemmas in connection tableau calculi ⋮ Model elimination without contrapositives ⋮ Prolog technology for default reasoning: proof theory and compilation techniques ⋮ Automatic verification of cryptographic protocols with SETHEO ⋮ Lemma matching for a PTTP-based top-down theorem prover ⋮ Hyper tableaux ⋮ The proof complexity of analytic and clausal tableaux ⋮ Practically useful variants of definitional translations to normal form ⋮ From Schütte’s Formal Systems to Modern Automated Deduction

Uses Software

• SETHEO
• TPTP
• METEOR

Cites Work

• The foundations of mathematics. A study in the philosophy of science
• 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
• The TPTP problem library. CNF release v1. 2. 1
• Controlled integration of the cut rule into connection tableau calculi
• Linear resolution with selection function
• An improved proof procedure1
• On Matrices with Connections
• Resolution, Refinements, and Search Strategies: A Comparative Study
• Mechanical Theorem-Proving by Model Elimination
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• A Unifying View of Some Linear Herbrand Procedures
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Controlled integration of the cut rule into connection tableau calculi