# Range-Restricted Interpolation through Clausal Tableaux

arXiv: https://arxiv.org/abs/2306.03572 · HTML: https://mlsanity.com/paper/2306.03572/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 67 references that are in the map.
- First posted on arXiv 6 Jun 2023.

## Builds on (most cited first, 6 of 6)

- [Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic](https://mlsanity.com/paper/2002.10892/) (2020)
- [Learning from Lukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)](https://mlsanity.com/paper/2104.13645/) (2021)
- [Craig Interpolation with Clausal First-Order Tableaux](https://mlsanity.com/paper/2008.03489/) (2020)
- [Lemmas: Generation, Selection, Application](https://mlsanity.com/paper/2303.05854/) (2023)
- [Blocking and Other Enhancements for Bottom-Up Model Generation Methods](https://mlsanity.com/paper/1611.09014/) (2016)
- [Synthesizing Nested Relational Queries from Implicit Specifications](https://mlsanity.com/paper/2209.08299/) (2022)

## Abstract (arXiv)

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.