Range-restricted and Horn interpolation through clausal tableaux

Cites Work

Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
An interpolation theorem in the predicate calculus
The road to two theorems of logic
Proof theory. 2nd ed
A structure-preserving clause form translation
A Prolog technology theorem prover: Implementation by an extended Prolog compiler
Logic for improving integrity checking in relational data bases
SETHEO: A high-performance theorem prover
IeanCOP: lean connection-based theorem proving
Positive unit hyperresolution tableaux and their application to minimal model generation
Learning from Łukasiewicz and Meredith: investigations into proof structures
Blocking and other enhancements for bottom-up model generation methods
Faster, higher, stronger: E 2.3
On interpolation in automated theorem proving
Craig interpolation with clausal first-order tableaux
Tableaux and related methods
Model elimination and connection tableau procedures
First-order tableau methods
Generating plans from proofs. The interpolation-based approach to query reformulation
Exact query reformulation over databases with first-order and description logics ontologies
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
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
On Enumerating Query Plans Using Analytic Tableau
Restricting backtracking in connection calculi
Fragments of first order logic, I: universal Horn logic
Syntactical characterization of a subset of domain-independent formulas
First-Order Interpolation and Interpolating Proof Systems
From Schütte’s Formal Systems to Modern Automated Deduction
Hyper tableaux
A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
Automatic Theorem Proving With Renamable and Semantic Resolution
Interpolation and Symbol Elimination in Vampire
Constructing Craig interpolation formulas
The 11th IJCAR automated theorem proving system competition – CASC-J11
Lemmas: generation, selection, application

This page was built for publication: Range-restricted and Horn interpolation through clausal tableaux

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6541142)