Range-restricted and Horn interpolation through clausal tableaux

Cites Work

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