{"@context":"https:\/\/schema.org\/","@type":"ScholarlyArticle","@id":"#article9977","name":"First-Order Interpolation and Grey Areas of Proofs (Invited Talk)","abstract":"Interpolation is an important technique in computer aided verification and static analysis of programs. In particular, interpolants extracted from so-called local proofs are used in invariant generation and bounded model checking. An interpolant extracted from such a proof is a boolean combination of formulas occurring in the proof. \r\n\r\nIn this talk we first describe a technique of generating and optimizing interpolants based on transformations of what we call the \u201cgrey area\u201d of local proofs. Local changes in proofs can change the extracted interpolant. Our method can describe properties of extracted interpolants obtained by such proof changes as a pseudo-boolean constraint. By optimizing solutions of this constraint we also improve the extracted interpolants. Unlike many other interpolation techniques, our technique is very general and applies to arbitrary theories. Our approach is implemented in the theorem prover Vampire and evaluated on a large number of benchmarks coming from first-order theorem proving and bounded model checking using logic with equality, uninterpreted functions and linear integer arithmetic. Our experiments demonstrate the power of the new techniques: for example, it is not unusual that our proof transformation gives more than a tenfold reduction in the size of interpolants.\r\n\r\nWhile local proofs admit efficient interpolation algorithms, standard complete proof systems, such as superposition, \r\nfor theories having the interpolation property are not necessarily complete for local proofs.\r\nIn this talk we therefore also investigate interpolant extraction from non-local proofs 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. 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.","keywords":["theorem proving","interpolation","proof transformations","constraint solving","program analysis"],"author":{"@type":"Person","name":"Kov\u00e1cs, Laura","givenName":"Laura","familyName":"Kov\u00e1cs"},"position":3,"pageStart":"3:1","pageEnd":"3:1","dateCreated":"2017-08-16","datePublished":"2017-08-16","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/3.0\/legalcode","copyrightHolder":{"@type":"Person","name":"Kov\u00e1cs, Laura","givenName":"Laura","familyName":"Kov\u00e1cs"},"copyrightYear":"2017","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2017.3","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":{"@type":"PublicationVolume","@id":"#volume6285","volumeNumber":82,"name":"26th EACSL Annual Conference on Computer Science Logic (CSL 2017)","dateCreated":"2017-08-16","datePublished":"2017-08-16","editor":[{"@type":"Person","name":"Goranko, Valentin","givenName":"Valentin","familyName":"Goranko"},{"@type":"Person","name":"Dam, Mads","givenName":"Mads","familyName":"Dam"}],"isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#article9977","isPartOf":{"@type":"Periodical","@id":"#series116","name":"Leibniz International Proceedings in Informatics","issn":"1868-8969","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#volume6285"}}}