Craig interpolation with clausal first-order tableaux
From MaRDI portal
Publication:2666953
DOI10.1007/s10817-021-09590-3OpenAlexW3047642368MaRDI QIDQ2666953
Publication date: 23 November 2021
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2008.03489
Craig interpolationconnection methodfirst-order theorem provingclausal tableauxinductive interpolationinterpolant liftingsimulation between calculitwo-stage interpolation
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interpolation systems for ground proofs in automated deduction: a survey
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Data exchange: semantics and query answering
- Methods of cut-elimination
- An interpolation theorem in the predicate calculus
- Comparing instance generation methods for automated reasoning
- The road to two theorems of logic
- A structure-preserving clause form translation
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- SETHEO: A high-performance theorem prover
- Controlled integration of the cut rule into connection tableau calculi
- Blocking and other enhancements for bottom-up model generation methods
- Faster, higher, stronger: E 2.3
- On interpolation in automated theorem proving
- A unifying principle for clause elimination in first-order logic
- An interpolating theorem prover
- Generating Plans from Proofs: The Interpolation-based Approach to Query Reformulation
- Acyclicity Notions for Existential Rules and Their Application to Query Answering in Ontologies
- Rewriting Guarded Negation Queries
- On Interpolation in Decision Procedures
- Database Repairing and Consistent Query Answering
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Efficient Low-Level Connection Tableaux
- On Enumerating Query Plans Using Analytic Tableau
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Blocked Clause Elimination
- Restricting backtracking in connection calculi
- System Description: E- KRHyper
- Hypertableau Reasoning for Description Logics
- Equality and lyndon's interpolation theorem
- Proving Theorems with the Modification Method
- Blocked Clauses in First-Order Logic
- First-Order Interpolation and Interpolating Proof Systems
- System Description: E-KRHyper 1.4
- Hyper tableaux
- The DLV system for knowledge representation and reasoning
- The MathSAT5 SMT Solver
- Logics in Artificial Intelligence
- Tools and Algorithms for the Construction and Analysis of Systems
- Theory and Applications of Satisfiability Testing
- Computer Aided Verification
This page was built for publication: Craig interpolation with clausal first-order tableaux
