Range-restricted and Horn interpolation through clausal tableaux

Cites work

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

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)