First-Order Interpolation and Interpolating Proofs Systems

Laura Kovacs, Andrei Voronkov

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

It is known that one can extract Craig interpolants from so-called local derivations. An interpolant extracted from such a derivation is a boolean combination of formulas occurring in the derivation. However, standard complete proof systems, such as superposition, for theories having the interpolation property are not necessarily complete for local proofs. In this paper we investigate interpolant extraction from non-local refutations (proofs of contradiction) in the superposition calculus and prove a number of general results about interpolant extraction and complexity of extracted interpolants. In particular, we prove that the number of quantifier alternations in first-order interpolants of formulas without quantifier alternations is unbounded. The proof of this result relies on a small number of assumptions about the theory and the proof system, so it also applies to many first-order theories beyond predicate logic. This result has far-reaching consequences for using local proofs as a foundation for interpolating proof systems - any such proof system should deal with formulas of arbitrary quantifier complexity. To search for alternatives for interpolating proof systems, we consider several variations on interpolation and local proofs. Namely, we give an algorithm for building interpolants from resolution refutations in logic without equality and discuss additional constraints when this approach can be also used for logic with equality. We finally propose a new direction related to interpolation via local proofs in first-order theories.
Original languageEnglish
Title of host publicationLPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Volume46
DOIs
Publication statusPublished - 4 May 2017
EventLPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Maun, Botswana
Duration: 7 May 201712 May 2017

Conference

ConferenceLPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Country/TerritoryBotswana
CityMaun
Period7/05/1712/05/17

Fingerprint

Dive into the research topics of 'First-Order Interpolation and Interpolating Proofs Systems'. Together they form a unique fingerprint.

Cite this