{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T19:40:19Z","timestamp":1750534819210},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>It is known that one can extract Craig interpolants from so-called local<\/jats:p><jats:p>proofs. An interpolant extracted from such a proof is a boolean<\/jats:p><jats:p>combination of formulas occurring in the proof. However, standard complete<\/jats:p><jats:p>proof systems, such as superposition, for theories having the interpolation<\/jats:p><jats:p>property are not necessarily complete for local proofs: there are formulas<\/jats:p><jats:p>having non-local proofs but no local proof.<\/jats:p><jats:p>In this paper we investigate interpolant extraction from non-local refutations<\/jats:p><jats:p>(proofs of contradiction) in the superposition calculus and prove a number<\/jats:p><jats:p>of general results about interpolant extraction and complexity of extracted<\/jats:p><jats:p>interpolants. In particular, we prove that the number of quantifier alternations<\/jats:p><jats:p>in first-order interpolants of formulas without quantifier alternations is<\/jats:p><jats:p>unbounded. This result has far-reaching consequences for using local proofs<\/jats:p><jats:p>as a foundation for interpolating proof systems: any such proof system should<\/jats:p><jats:p>deal with formulas of arbitrary quantifier complexity.<\/jats:p><jats:p>To search for alternatives for interpolating proof systems, we consider several<\/jats:p><jats:p>variations on interpolation and local proofs. Namely, we give an algorithm for<\/jats:p><jats:p>building interpolants from resolution refutations in logic without equality and<\/jats:p><jats:p>discuss additional constraints when this approach can be also used for logic<\/jats:p><jats:p>with equality. We finally propose a new direction related to interpolation via<\/jats:p><jats:p>local proofs in first-order theories.<\/jats:p>","DOI":"10.29007\/1qb8","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:04:37Z","timestamp":1516730677000},"page":"49-32","source":"Crossref","is-referenced-by-count":4,"title":["First-Order Interpolation and Interpolating Proof Systems"],"prefix":"10.29007","volume":"46","author":[{"given":"Laura","family":"Kov\u00e1cs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"11545","event":{"name":"LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:04:39Z","timestamp":1516730679000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/r2J"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/1qb8","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}