Range-Restricted Interpolation through Clausal Tableaux

We show how variations of range-restriction and also the Horn property can be passed from inputs to outputs of Craig interpolation in first-order logic. The proof system is clausal tableaux, which stems from first-order ATP. Our results are induced by a restriction of the clausal tableau structure, which can be achieved in general by a proof transformation, also if the source proof is by resolution/paramodulation. Primarily addressed applications are query synthesis and reformulation with interpolation. Our methodical approach combines operations on proof structures with the immediate perspective of feasible implementation through incorporating highly optimized first-order provers.

• Publication year

  2023

• Venue

  International Conference on Theorem Proving with Analytic Tableaux and Related Methods

• Publication date

  2023-06-06

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/978-3-031-43513-3_1arXiv 2306.03572
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Lemmas: Generation, Selection, Application

  2023cited by this paper
• The 11th IJCAR automated theorem proving system competition – CASC-J11

  2023influential reference
• Synthesizing Nested Relational Queries from Implicit Specifications

  2022cited by this paper
• Learning from Łukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)

  2021cited by this paper
• Craig Interpolation with Clausal First-Order Tableaux

  2020influential reference
• Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic

  2020influential reference
• From Schütte’s Formal Systems to Modern Automated Deduction

  2020cited by this paper
• Faster, Higher, Stronger: E 2.3

  2019cited by this paper
• First-Order Interpolation and Interpolating Proof Systems

  2017cited by this paper
• An Interpolation-based Compiler and Optimizer for Relational Queries (System design Report)

  2017cited by this paper
• Proof Theory

  2017cited by this paper
• First-Order Logic

  2017cited by this paper
• Reformulating Queries: Theory and Practice

  2017cited by this paper
• Generating Plans from Proofs: The Interpolation-based Approach to Query Reformulation

  2016cited by this paper
• On Enumerating Query Plans Using Analytic Tableau

  2015cited by this paper
• On Interpolation in Automated Theorem Proving

  2014cited by this paper
• First-Order Theorem Proving and Vampire

  2013cited by this paper
• Exact Query Reformulation over Databases with First-order and Description Logics Ontologies

  2013cited by this paper
• Vinter: A Vampire-Based Tool for Interpolation

  2012cited by this paper
• Fundamentals of Physical Design and Query Compilation

  2011cited by this paper
• Interpolation and Symbol Elimination in Vampire

  2010cited by this paper
• Restricting backtracking in connection calculi

  2010cited by this paper
• Views and queries: Determinacy and rewriting

  2010cited by this paper
• Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic

  2010cited by this paper
• The road to two theorems of logic

  2008cited by this paper
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic

  2008cited by this paper
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods

  2006cited by this paper
• Automated Theorem Proving

  2004cited by this paper
• leanCoP: lean connection-based theorem proving

  2003cited by this paper
• Tableaux and Related Methods

  2001cited by this paper
• Model Elimination and Connection Tableau Procedures

  2001cited by this paper
• Positive Unit Hyperresolution Tableaux and Their Application to Minimal Model Generation

  2000cited by this paper
• First-Order Tableau Methods

  1999cited by this paper
• Hyper Tableaux

  1996cited by this paper
• Constructing Craig Interpolation Formulas

  1995cited by this paper
• Foundations of Databases

  1994cited by this paper
• Syntactical characterization of a subset of domain-independent formulas

  1992cited by this paper
• SETHEO: A high-performance theorem prover

  1992cited by this paper
• Safety and translation of relational calculus

  1991cited by this paper
• First-Order Logic and Automated Theorem Proving

  1990cited by this paper
• Logic for Improving Integrity Checking in Relational Data Bases

  1989cited by this paper
• SATCHMO: A Theorem Prover Implemented in Prolog

  1988cited by this paper
• A prolog technology theorem prover: Implementation by an extended prolog compiler

  1986cited by this paper
• A Structure-Preserving Clause Form Translation

  1986cited by this paper
• An Implementation of a Theorem Prover Based on the Connection Method

  1984cited by this paper
• Automatic Deduction with Hyper-Resolution

  1983cited by this paper
• On the Complexity of Derivation in Propositional Calculus

  1983cited by this paper
• Automated theorem proving: a logical basis

  1978cited by this paper
• Fragments of first order logic, I: universal Horn logic

  1977cited by this paper
• Automatic Theorem Proving With Renamable and Semantic Resolution

  1967cited by this paper
• An interpolation theorem in the predicate calculus.

  1959cited by this paper
• Linear reasoning. A new form of the Herbrand-Gentzen theorem

  1957cited by this paper
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

  1957cited by this paper
• Under Consideration for Publication in Theory and Practice of Logic Programming Swi-prolog

  year unknowncited by this paper

• A Review of Medical Data Sources, and Advanced Data Analytics in the Medical Sector

  2023cites this paper