×

zbMATH — the first resource for mathematics

Labelled interpolation systems for hyper-resolution, clausal, and local proofs. (English) Zbl 1356.68199
Summary: Craig’s interpolation theorem has numerous applications in model checking, automated reasoning, and synthesis. There is a variety of interpolation systems which derive interpolants from refutation proofs; these systems are ad-hoc and rigid in the sense that they provide exactly one interpolant for a given proof. In previous work, we introduced a parametrised interpolation system which subsumes existing interpolation methods for propositional resolution proofs and enables the systematic variation of the logical strength and the elimination of non-essential variables in interpolants. In this paper, we generalise this system to propositional hyper-resolution proofs as well as clausal proofs. The latter are generated by contemporary SAT solvers. Finally, we show that, when applied to local (or split) proofs, our extension generalises two existing interpolation systems for first-order logic and relates them in logical strength.
MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
03C40 Interpolation, preservation, definability
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Andrews, PB, Resolution with merging, J. ACM, 15, 367-381, (1968) · Zbl 0182.02506
[2] Bacchus, F.: Enhancing davis putnam with extended binary clause reasoning. In: Eighteenth National Conference on Artificial Intelligence, pp. 613-619. American Association for Artificial Intelligence, Menlo Park (2002) · Zbl 0081.24402
[3] Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-time reductions of resolution proofs. Technical Report IE/IS-2008-02, Technion (2008) · Zbl 1159.68403
[4] Beame, P; Kautz, H; Sabharwal, A, Towards understanding and harnessing the potential of clause learning, J. Artif. Intell. Res., 22, 319-351, (2004) · Zbl 1080.68651
[5] Biere, A, Picosat essentials, JSAT, 4, 75-97, (2008) · Zbl 1159.68403
[6] Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T.: Handbook of Satisfiability, Volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press (2009) · Zbl 1183.68568
[7] Bloem, R; Galler, S; Jobstmann, B; Piterman, N; Pnueli, A; Weiglhofer, M, Specify, compile, run: hardware from psl, Electron. Notes Theor. Comput. Sci., 190, 3-16, (2007)
[8] Bloem, R., Könighofer, R., Seidl, M.: Sat-based synthesis methods for safety specs. In: McMillan, K., Rival, X. (eds.) VMCAI, Volume 8318 of LNCS, pp. 1-20. Springer, Berlin (2014) · Zbl 1428.68040
[9] Bloem, R., Malik, S., Schlaipfer, M., Weissenbacher, G.: Reduction of resolution refutations and interpolants via subsumption. In: Haifa Verification Conference, pp. 188. Springer (2014)
[10] Bonacina, M.P., Johansson, M.: On interpolation in decision procedures. In: TABLEAUX, Volume 6793 of LNCS, pp. 1-16. Springer (2011) · Zbl 1331.68198
[11] Bradley, A.R.: SAT-based model checking without unrolling. In: VMCAI, Volume 6538 of LNCS, pp. 70-87. Springer (2011) · Zbl 1317.68109
[12] Brayton, R., Mishchenko, A.: ABC: An academic industrial-strength verification tool. In: CAV, Volume 6174 of LNCS, pp. 24-40. Springer (2010)
[13] Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Logic, 12(1), 1-54 (2010) · Zbl 1351.68247
[14] Craig, W, Linear reasoning. A new form of the Herbrand-Gentzen theorem, J. Symb. Log., 22, 250-268, (1957) · Zbl 0081.24402
[15] D’Silva, V.: Propositional interpolation and abstract interpretation. In: European Symposium on Programming, Volume 6012 of LNCS. Springer (2010)
[16] D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: VMCAI, Volume 5944 of LNCS, pp. 129-145. Springer (2010) · Zbl 1273.68225
[17] Eén, N., Sörensson, N.: An extensible SAT-solver. In: SAT, Volume 2919, pp. 502-518. Springer (2004) · Zbl 1204.68191
[18] Ermis, E., Schäf, M., Wies, T.: Error invariants. In: Formal Methods, Volume 7436 of LNCS, pp. 187-201. Springer (2012) · Zbl 1372.68061
[19] Fontaine, P., Merz, S., Paleo, B.W.: Compression of propositional resolution proofs via partial regularization. In: CADE, Volume 6803 of LNCS. Springer (2011) · Zbl 1341.68188
[20] Fuchs, A., Goel, A., Grundy, J., Krstić, S., Tinelli, C.: Ground interpolation for the theory of equality. In: TACAS, Volume 5005 of LNCS, pp. 413-427. Springer (2009) · Zbl 1234.68257
[21] Gershman, R., Strichman, O.: Cost-effective hyper-resolution for preprocessing cnf formulas. In: SAT, Volume 3569 of LNCS, pp. 423-429. Springer (2005) · Zbl 1128.68465
[22] Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE, pp. 886-891. IEEE (2003)
[23] Gupta, A., Popeea, C., Rybalchenko, A.: Generalised interpolation by solving recursion-free Horn clauses. CoRR, abs/1303.7378 (2013)
[24] Gurfinkel, A., Vizel, Y.: Druping for interpolants. In: Formal Methods in Computer-Aided Design, pp. 99-106. FMCAD Inc. (2014)
[25] Heule, M., W.A.H. Jr., Wetzler, N.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, pp. 181-188. IEEE (2013) · Zbl 0945.03086
[26] Hoder, K., Kovács, L., Voronkov, A.: Playing in the grey area of proofs. In: Principles of Programming Languages, pp. 259-272. ACM (2012) · Zbl 1321.68196
[27] Hofferek, G., Gupta, A., Könighofer, B., Jiang, J.R., Bloem, R.: Synthesizing multiple boolean functions using interpolation on a single proof. In: Formal Methods in Computer-Aided Design, pp. 77-84. IEEE (2013)
[28] Huang, G.: Constructing Craig interpolation formulas. In: Computing and Combinatorics, Volume 959 of LNCS, pp. 181-190. Springer (1995)
[29] Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: CAV, Volume 3576 of LNCS, pp. 39-51. Springer (2005) · Zbl 1081.68622
[30] Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: TACAS, Volume 3920 of LNCS, pp. 459-473. Springer (2006) · Zbl 1180.68118
[31] Jiang, J.-H.R., Lin, H.-P., Hung, W.-L.: Interpolating functions from large Boolean relations. In: ICCAD, pp. 779-784. ACM (2009) · Zbl 1080.68651
[32] Kovács, L., Voronkov, A.: Interpolation and symbol elimination. In: CADE, Volume 5663 of LNCS, pp. 199-213. Springer (2009) · Zbl 1250.68193
[33] Krajíček, J, Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. Symb. Log., 62, 457-486, (1997) · Zbl 0891.03029
[34] Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Texts in Theoretical Computer Science. Springer (2008) · Zbl 1149.68071
[35] Kroening, D., Weissenbacher, G.: Lifting propositional interpolants to the word-level. In: Formal Methods in Computer-Aided Design, pp. 85-89. IEEE (2007)
[36] Kroening, D., Weissenbacher, G.: An interpolating decision procedure for transitive relations with uninterpreted functions. In: Haifa Verification Conference, Volume 6405 of LNCS, pp. 150-168. Springer (2011)
[37] Maehara, S, On the interpolation theorem of Craig, Sûgaku, 12, 235-237, (1961) · Zbl 0123.24601
[38] Malik, S., Weissenbacher, G.: Boolean satisfiability solvers: techniques and extensions. In: Software Safety and Security—Tools for Analysis and Verification, NATO Science for Peace and Security Series. IOS Press (2012)
[39] McMillan, K.L.: Interpolation and SAT-based model checking. In: CAV, Volume 2725 of LNCS, pp. 1-13. Springer (2003) · Zbl 1278.68184
[40] McMillan, KL, An interpolating theorem prover, Theor. Comput. Sci., 345, 101-121, (2005) · Zbl 1079.68092
[41] McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: TACAS, Volume 4963 of LNCS, pp. 413-427. Springer (2008) · Zbl 1134.68416
[42] Pudlák, P, Lower bounds for resolution and cutting plane proofs and monotone computations, J. Symb. Log., 62, 981-998, (1997) · Zbl 0945.03086
[43] Robinson, J.: Automatic deduction with hyper-resolution. J. Comput. Math. 1, 227-234 (1965) · Zbl 0158.26003
[44] Rollini, S.F., Alt, L., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N.: PeRIPLO: A framework for producing effective interpolants in SAT-based software verification. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Volume 8312 of LNCS, pp. 683-693. Springer (2013) · Zbl 1407.68303
[45] Rollini, SF; Bruttomesso, R; Sharygina, N; Tsitovich, A, Resolution proof transformation for compression and interpolation, Form. Methods Syst. Des., 45, 1-41, (2014) · Zbl 1317.68123
[46] Rollini, S.F., Sery, O., Sharygina, N.: Leveraging interpolant strength in model checking. In: CAV, Volume 7358 of LNCS, pp. 193-209. Springer (2012) · Zbl 0891.03029
[47] Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: VMCAI, Volume 4349 of LNCS, pp. 346-362. Springer (2007) · Zbl 1132.68480
[48] Sharma, R., Nori, A., Aiken, A.: Interpolants as classifiers. In: Madhusudan, P., Seshia, S., (eds.) CAV, Volume 7358 of LNCS, pp. 71-87. Springer, Berlin (2012)
[49] Silva, J.P.M., Sakallah, K.A.: GRASP—a new search algorithm for satisfiability. In: ICCAD, pp. 220-227 (1996)
[50] Simmonds, J; Davies, J; Gurfinkel, A; Chechik, M, Exploiting resolution proofs to speed up LTL vacuity detection for BMC, STTT, 12, 319-335, (2010)
[51] Sofronie-Stokkermans, V.: Interpolation in local theory extensions. In: Automated Reasoning, pp. 235-250. Springer (2006) · Zbl 1222.03018
[52] Totla, N., Wies, T.: Complete instantiation-based interpolation. In: Principles of Programming Languages, pp. 537-548. ACM, New York (2013) · Zbl 1301.68106
[53] Vizel, Y., Ryvchin, V., Nadel, A: Efficient generation of small interpolants in CNF. In: CAV, Volume 8044 of LNCS, pp. 330-346. Springer (2013) · Zbl 1341.68120
[54] Vizel, Y; Weissenbacher, G; Malik, S, Boolean satisfiability solvers and their applications in model checking, Proc. IEEE, 103, 2021-2035, (2015)
[55] Weissenbacher, G: Program Analysis with Interpolants. Ph.D. thesis, Oxford (2010) · Zbl 0123.24601
[56] Weissenbacher, G: Interpolant strength revisited. In: SAT, Volume 7317 of LNCS, pp. 312-326. Springer (2012) · Zbl 1273.03051
[57] Weissenbacher, G: Explaining heisenbugs. In: Runtime Verification, Volume 9333 of LNCS, p. XV. Springer (2015) · Zbl 1079.68092
[58] Yorsh, G., Musuvathi, M: A combination method for generating interpolants. In: CADE, Volume 3632 of LNCS, pp. 353-368 (2005) · Zbl 1135.03331
[59] Zhu, C.S., Weissenbacher, G., Malik, S: Silicon fault diagnosis using sequence interpolation with backbones. In: ICCAD, pp. 348-355. IEEE (2014) · Zbl 1317.68123
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.