{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T23:48:15Z","timestamp":1649202495492},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"It is known that one can extract Craig interpolants from so-called local<\/jats:p>proofs. An interpolant extracted from such a proof is a boolean<\/jats:p>combination of formulas occurring in the proof. However, standard complete<\/jats:p>proof systems, such as superposition, for theories having the interpolation<\/jats:p>property are not necessarily complete for local proofs: there are formulas<\/jats:p>having non-local proofs but no local proof.<\/jats:p>In this paper we investigate interpolant extraction from non-local refutations<\/jats:p>(proofs of contradiction) in the superposition calculus and prove a number<\/jats:p>of general results about interpolant extraction and complexity of extracted<\/jats:p>interpolants. In particular, we prove that the number of quantifier alternations<\/jats:p>in first-order interpolants of formulas without quantifier alternations is<\/jats:p>unbounded. This result has far-reaching consequences for using local proofs<\/jats:p>as a foundation for interpolating proof systems: any such proof system should<\/jats:p>deal with formulas of arbitrary quantifier complexity.<\/jats:p>To search for alternatives for interpolating proof systems, we consider several<\/jats:p>variations on interpolation and local proofs. Namely, we give an algorithm for<\/jats:p>building interpolants from resolution refutations in logic without equality and<\/jats:p>discuss additional constraints when this approach can be also used for logic<\/jats:p>with equality. We finally propose a new direction related to interpolation via<\/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-23T23:04:37Z","timestamp":1516748677000},"source":"Crossref","is-referenced-by-count":0,"title":["First-Order Interpolation and Interpolating Proof Systems"],"prefix":"10.29007","author":[{"given":"Laura","family":"Kov\u00e1cs","sequence":"first","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"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-23T23:04:39Z","timestamp":1516748679000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/r2J"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"http:\/\/dx.doi.org\/10.29007\/1qb8","relation":{},"ISSN":["2398-7340"],"issn-type":[{"value":"2398-7340","type":"print"}]}}