Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Reasoning About Concurrency in High-Assurance, High-Performance Software Systems Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Splitting Proofs for Interpolation

Authors : Bernhard Gleiss, Laura Kovács, Martin Suda

Published in: Automated Deduction – CADE 26

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We study interpolant extraction from local first-order refutations. We present a new theoretical perspective on interpolation based on clearly separating the condition on logical strength of the formula from the requirement on the common signature. This allows us to highlight the space of all interpolants that can be extracted from a refutation as a space of simple choices on how to split the refutation into two parts. We use this new insight to develop an algorithm for extracting interpolants which are linear in the size of the input refutation and can be further optimized using metrics such as number of non-logical symbols or quantifiers. We implemented the new algorithm in first-order theorem prover Vampire and evaluated it on a large number of examples coming from the first-order proving community. Our experiments give practical evidence that our work improves the state-of-the-art in first-order interpolation.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter A Unifying Principle for Clause Elimination in First-Order Logic
next chapter Detecting Inconsistencies in Large First-Order Knowledge Bases
Footnotes
1
This could potentially be violated by an advanced transformation based on formula sharing. In particular, the case would need to involve a common sub-formula of A and \(\lnot B\).
 
2
Note that the symbols are global with respect to A and B if and only if they are global with respect to \(\mathcal {C}_A\) and \(\mathcal {C}_{\lnot B}\) thanks to the requirement (1).
 
3
Bonacina and Johansson [2] introduce the notion of a provisional interpolant with an analogous definition. However, the intended use of the notion is different. While provisional interpolants are meant to be modified to yield interpolants in a refinement stage, we give conditions under which intermediants are, in fact, interpolants.
 
4
The executables and connecting scripts used in the experiment are available at http://​forsyte.​at/​static/​people/​suda/​vampire_​new_​interpolation.​zip.
 
5
SEOpt uses the SMT solver Yices [8] (version 1.0) and communicates via a file, while LinOpt one relies on Z3 [7] (version 4.5) and its API.
 
6
An interesting side-effect is an ability of SEOpt to assign two different colors to a formula when considered from the perspective of two different sub-derivations. In rare cases, such formula does not need to appear at all, and the final interpolant may be smaller than what is achievable by LinOpt. An instance of this phenomenon occurred in our experiment on benchmark SYN577-1, which appears in Fig. 6 (left) slightly above the diagonal.
 
Literature
1.
Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 46–61. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-28717-6_​7 CrossRef
2.
3.
Christ, J., Hoenicke, J.: Instantiation-based interpolation for quantified formulae. In: Decision Procedures in Software, Hardware and Bioware, April 18–23 April 2010, vol. 10161. Dagstuhl Seminar Proceedings. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany (2010)
4.
5.
Cimatti, A., Griggio, A., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 397–412. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-78800-3_​30 CrossRef
6.
7.
8.
9.
Hoder, K., Kovács, L., Voronkov, A.: Playing in the grey area of proofs. In: Principles of Programming Languages, pp. 259–272. ACM (2012)
10.
Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006). doi:10.​1007/​11691372_​33 CrossRef
11.
12.
13.
Kovács, L., Voronkov, A.: First-order interpolation and interpolating proof systems. In: LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol. 46. EPiC Series in Computing, pp. 49–64. EasyChair (2017)
14.
Lahiri, S.K., Mehra, K.K.: Interpolant based decision procedure for quantifier-free Presburger arithmetic. Technical Report MSR-TR-2005-121, Microsoft Research (2005)
15.
16.
17.
McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413–427. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-78800-3_​31 CrossRef
18.
Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning, vol. 2s, pp. 335–367. Elsevier and MIT Press (2001)
19.
Podelski, A., Schäf, M., Wies, T.: Classifying bugs with interpolants. In: Aichernig, B.K.K., Furia, C.A.A. (eds.) TAP 2016. LNCS, vol. 9762, pp. 151–168. Springer, Cham (2016). doi:10.​1007/​978-3-319-41135-4_​9
20.
Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: GCAI 2016, 2nd Global Conference on Artificial Intelligence, vol. 41. EPiC Series in Computing, pp. 11–23. EasyChair (2016)
21.
22.
Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reasoning 43(4), 337–362 (2009)CrossRefMATH
23.
Totla, N., Wies, T.: Complete instantiation-based interpolation. In: Principles of Programming Languages, pp. 537–548. ACM (2013)
Metadata
Title
Splitting Proofs for Interpolation
Authors
Bernhard Gleiss
Laura Kovács
Martin Suda
Copyright Year
2017
Book
Automated Deduction – CADE 26

Print ISBN: 978-3-319-63045-8

Electronic ISBN: 978-3-319-63046-5

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-63046-5_18

Premium Partner

    Image Credits