Range-Restricted Interpolation through Clausal Tableaux

Christoph Wernhard
6/6/2023
cs.LOcs.AIcs.DB

No confident code implementation found for this paper.

Abstract

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.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)

76% match2022

INDUCTION: Finite-Structure Concept Synthesis in First-Order Logic

74% match2026

SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning

74% match2023

On Exact Sampling in the Two-Variable Fragment of First-Order Logic

73% match2023

The Lindstrom's Characterizability of Abstract Logic Systems for Analytic Structures Based on Measures

72% match2023

Investigations into Proof Structures

72% match2023

Cite this paper

@article{wernhard2023rangerestricted,
  title  = {Range-Restricted Interpolation through Clausal Tableaux},
  author = {Christoph Wernhard},
  year   = {2023},
  eprint = {2306.03572},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2306.03572v3}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2306.03572.svg)](https://codeofpaper.com/paper/2306.03572)

Discussion