×

zbMATH — the first resource for mathematics

Data compression for proof replay. (English) Zbl 1191.68616
Summary: We describe a compressing translation from SAT solver generated propositional resolution refutation proofs to classical natural deduction proofs. The resulting proof can usually be checked quicker than one that simply simulates the original resolution proof. We use this result in interactive theorem provers, to speed up reconstruction of SAT solver generated proofs. The translation is fast and scales up to large proofs with millions of inferences.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W[P] is tractable. In: FOCS, pp. 210–219. IEEE, Piscataway (2001) · Zbl 1169.03044
[2] Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, R. (ed.) Tools and Algorithms for Construction and Analysis of Systems. LNCS, vol. 1579. Springer, New York (1999)
[3] Bryant, R.E., Lahiri, S., Seshia, S.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) Proc. 14th Intl. Conference on Computer Aided Verification. LNCS, vol. 2404, pp. 78–92. Springer, New York (2002) · Zbl 1010.68522
[4] Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004). LNCS, vol. 2988, pp. 168–176. Springer, New York (2004) · Zbl 1126.68470
[5] Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT, Cambridge (2001) · Zbl 1047.68161
[6] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. J. Assoc. Comput. Mach. 5(7), 394–397 (1962) · Zbl 0217.54002
[7] Diestel, R.: Graph Theory. Springer, New York (2005) · Zbl 1074.05001
[8] Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing, 6th International Conference. LNCS, vol. 2919, pp. 502–518. Springer, New York (2003) · Zbl 1204.68191
[9] Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS. LNCS, vol. 3920, pp. 167–181. Springer, New York (2006) · Zbl 1180.68240
[10] Gershman, R., Koifman, M., Strichman, O.: Deriving small unsatisfiable cores with dominators. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification. LNCS, vol. 4144, pp. 109–122. Springer, New York (2006)
[11] Gordon, M.J.C., Melham, T.F. (eds.) Introduction to HOL: a Theorem-Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993) · Zbl 0779.68007
[12] Gusfield, D.: Algorithmson String, Trees, and Sequences. Cambridge University Press, Cambridge (1997) · Zbl 0934.68103
[13] Harel, D., Tarjan, R.E.: Fast algorithms for finding nearest common ancestors. SIAM J. Comput. 13(2), 338–355 (1984) · Zbl 0535.68022 · doi:10.1137/0213024
[14] Harrison, J.: Metatheory and Reflection in Theorem Proving: a Survey and Critique. Technical Report CRC-053, SRI International (1995)
[15] Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M.K., Camilleri, A.J. (eds.) FMCAD. LNCS, vol. 1166, pp. 265–269. Springer, New York (1996)
[16] Harrison, J.: Stålmarck’s algorithm as a HOL derived rule. In: von Wright, J., Grundy, J., Harrison, J. (eds.) Theorem Proving in Higher Order Logics. LNCS, vol. 1125, pp. 221–234. Springer, New York (1996)
[17] Hickey, J., Nogin, A., Constable, R.L., Aydemir, B.E., Barzilay, E., Bryukhov, Y., Eaton, R., Granicz, A., Kopylov, A., Kreitz, C., Krupski, V., Lorigo, L., Schmitt, S., Witty, C., Yu, X.: Metaprl–a modular logical environment. In: Basin, D.A., Wolff, B. (eds.) TPHOLs. LNCS, vol. 2758, pp. 287–303. Springer, New York (2003)
[18] Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq Proof Assistant: a Tutorial: Version 7.2. Technical Report RT-0256, INRIA (2002)
[19] Inenaga, S., Hoshino, H., Shinohara, A., Takeda, M., Arikawa, S., Mauri, G., Pavesi, G.: On-line construction of compact directed acyclic word graphs. Discrete Appl. Math. 146(2), 156–179 (2005) · Zbl 1084.68137 · doi:10.1016/j.dam.2004.04.012
[20] Mitchell, D.G.: A SAT solver primer. In: EATCS Bulletin. The Logic in Computer Science Column, vol. 85, pp. 112–133. Springer, New York (2005) · Zbl 1169.68444
[21] Morrison, D.R.: PATRICIA-practical algorithm to retrieve information coded in alphanumeric. J. Assoc. Comput. Mach. 15(4), 514–534 (1968)
[22] Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, pp. 530–535. ACM, New York (2001)
[23] Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) 11th International Conference on Automated Deduction (CADE). LNAI, vol. 607, pp. 748–752. Springer, New York (1992). http://pvs.csl.sri.com
[24] Paulson, L.C.: Isabelle: a Generic Theorem Prover. LNCS, vol. 828. Springer, New York (1994) · Zbl 0825.68059
[25] Shankar, N.: Using decision procedures with a higher-order logic. In: Boulton, R.J., Jackson, P.B. (eds.) Theorem Proving in Higher Order Logics, LNCS, vol. 2152, pp. 5–26. Springer, New York (2001) · Zbl 1005.68543
[26] Sinz, C.: Compressing propositional proofs by common subproof extraction. In: Pichler, F. (ed.) Euro Conference on Computer Aided Systems Theory, Las Palmas de Gran Canaria, 12–16 February 2007
[27] Ukkonen, E.: Online construction of suffix trees. Algorithmica 14(3), 249–260 (1995) · Zbl 0831.68027 · doi:10.1007/BF01206331
[28] Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. JAL (2008). doi: 10.1016/j.jal.2007.07.003 · Zbl 1171.68041
[29] Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: DATE, pp. 10880–10885. IEEE Computer Society, Los Alamitos (2003)
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.