Craig interpolation with clausal first-order tableaux. (English) Zbl 1543.03053
Summary: We develop foundations for computing Craig-Lyndon interpolants of two given formulas with first-order theorem provers that construct clausal tableaux. Provers that can be understood in this way include efficient machine-oriented systems based on calculi of two families: goal-oriented such as model elimination and the connection method, and bottom-up such as the hypertableau calculus. We present the first interpolation method for first-order proofs represented by closed tableaux that proceeds in two stages, similar to known interpolation methods for resolution proofs. The first stage is an induction on the tableau structure, which is sufficient to compute propositional interpolants. We show that this can linearly simulate different prominent propositional interpolation methods that operate by an induction on a resolution deduction tree. In the second stage, interpolant lifting, quantified variables that replace certain terms (constants and compound terms) by variables are introduced. We justify the correctness of interpolant lifting (for the case without built-in equality) abstractly on the basis of Herbrand’s theorem and for a different characterization of the formulas to be lifted than in the literature. In addition, we discuss various subtle aspects that are relevant for the investigation and practical realization of first-order interpolation based on clausal tableaux.
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 03C40 | Interpolation, preservation, definability |
Keywords:
Craig interpolation; first-order theorem proving; clausal tableaux; connection method; inductive interpolation; simulation between calculi; two-stage interpolation; interpolant liftingSoftware:
SATCHMO; E-SETHEO; Prover9; Mace4; SETHEO; Princess; MiniSat; FOCI; leanCoP; E-KRHyper; FEMaLeCoP; PTTP; MathSAT5; EasychairReferences:
| [1] | Baaz, M.; Leitsch, A., Methods of Cut-Elimination (2011), Berlin: Springer, Berlin · Zbl 1225.03075 |
| [2] | Bachmair, L., Ganzinger, H., Voronkov, A.: Elimination of equality via transformation with ordering constraints. In: CADE-15, LNCS (LNAI), vol. 1421, pp. 175-190. Springer (1998) · Zbl 0926.03006 |
| [3] | Baumgartner, P., Furbach, U., Niemelä, I.: Hyper tableaux. In: JELIA’96, LNCS (LNAI), vol. 1126, pp. 1-17. Springer (1996) · Zbl 1427.03031 |
| [4] | Baumgartner, P.; Schmidt, RA, Blocking and other enhancements for bottom-up model generation methods, J. Autom. Reason., 64, 197-251 (2020) · Zbl 1468.68279 · doi:10.1007/s10817-019-09515-1 |
| [5] | Baumgartner, P.; Thorstensen, E., Instance based methods – a brief overview, KI, 24, 1, 35-42 (2010) |
| [6] | Bender, M., Pelzer, B., Schon, C.: System description: E-KRHyper 1.4. In: CADE-24, LNCS (LNAI), vol. 7898, pp. 126-134. Springer (2013) · Zbl 1381.68258 |
| [7] | Benedikt, M., ten Cate, B., Tsamoura, E.: Generating low-cost plans from proofs. In: PODS’14, pp. 200-211. ACM (2014) |
| [8] | Benedikt, M., Kostylev, E.V., Mogavero, F., Tsamoura, E.: Reformulating queries: theory and practice. In: IJCAI 2017, pp. 837-843 (2017) |
| [9] | Benedikt, M.; Leblay, J.; ten Cate, B.; Tsamoura, E., Generating Plans from Proofs: The Interpolation-based Approach to Query Reformulation (2016), New York: Morgan & Claypool, New York · Zbl 1345.68003 · doi:10.1145/2847523 |
| [10] | Bibel, W.: Automated Theorem Proving. Vieweg (1982). Second edition 1987 · Zbl 0492.68067 |
| [11] | Bibel, W., Otten, J.: From Schütte’s formal systems to modern automated deduction. In: Kahle, R., Rathjen, M. (eds.) The Legacy of Kurt Schütte, chap. 13, pp. 215-249. Springer (2020) |
| [12] | Bonacina, M.P., Johansson, M.: On interpolation in decision procedures. In: TABLEAUX 2011, LNCS (LNAI), vol. 6793, pp. 1-16. Springer (2012) · Zbl 1331.68198 |
| [13] | Bonacina, MP; Johansson, M., Interpolation systems for ground proofs in automated deduction: a survey, J. Autom. Reason., 54, 4, 353-390 (2015) · Zbl 1356.68179 · doi:10.1007/s10817-015-9325-5 |
| [14] | Bonacina, MP; Johansson, M., On interpolation in automated theorem proving, J. Autom. Reason., 54, 1, 69-97 (2015) · Zbl 1315.03018 · doi:10.1007/s10817-014-9314-0 |
| [15] | Borgida, A., de Bruijn, J., Franconi, E., Seylan, I., Straccia, U., Toman, D., Weddell, G.: On finding query rewritings under expressive constraints. In: SEBD 2010. Esculapio Editore (2010) |
| [16] | Brand, D., Proving theorems with the modification method, SIAM J. Comput., 4, 4, 412-430 (1975) · Zbl 0333.68059 · doi:10.1137/0204036 |
| [17] | Brillout, A.; Kroening, D.; Rümmer, P.; Wahl, T., An interpolating sequent calculus for quantifier-free Presburger arithmetic, J. Autom. Reason., 47, 4, 341-367 (2011) · Zbl 1259.03043 · doi:10.1007/s10817-011-9237-y |
| [18] | Bry, F., Manthey, R.: SATCHMO: A theorem prover implemented in Prolog. In: CADE-9, LNCS, vol. 310, pp. 415-434. Springer (1988) · Zbl 0668.68104 |
| [19] | Bárány, V., Benedikt, M., ten Cate, B.: Rewriting guarded negation queries. In: MFCS 2013, LNCS, vol. 8087, pp. 98-110. Springer (2013) · Zbl 1398.68120 |
| [20] | Chang, CL; Lee, RCT, Symbolic Logic and Automated Theorem Proving (1973), Cambridge: Academic Press, Cambridge · Zbl 0263.68046 |
| [21] | Christ, J., Hoenicke, J.: Instantiation-based interpolation for quantified formulae. In: Decision Procedures in Software, Hardware and Bioware, vol. 10161. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010) |
| [22] | Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: TACAS 2013, LNCS, vol. 7795, pp. 93-107. Springer (2013) · Zbl 1381.68153 |
| [23] | Craig, W., Linear reasoning. A new form of the Herbrand-Gentzen theorem, J. Symb. Log., 22, 3, 250-268 (1957) · Zbl 0081.24402 · doi:10.2307/2963593 |
| [24] | Craig, W., Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, J. Symb. Log., 22, 3, 269-285 (1957) · Zbl 0079.24502 · doi:10.2307/2963594 |
| [25] | Craig, W., The road to two theorems of logic, Synthese, 164, 3, 333-339 (2008) · Zbl 1171.03017 · doi:10.1007/s11229-008-9353-3 |
| [26] | Dahn, I., Wernhard, C.: First order proof problems extracted from an article in the Mizar mathematical library. In: FTP’97, RISC-Linz Report Series No. 97-50, pp. 58-62. Joh. Kepler Univ., Linz, Austria (1997) |
| [27] | Dershowitz, N.; Jouannaud, J., Notations for rewriting, Bull. EATCS, 43, 162-174 (1991) · Zbl 0745.68115 |
| [28] | Eder, E.: An implementation of a theorem prover based on the connection method. In: AIMSA’84, pp. 121-128. North-Holland (1985) |
| [29] | Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: SAT ’05, LNCS, vol. 3569, pp. 61-75. Springer (2005) · Zbl 1128.68463 |
| [30] | Fagin, R.; Kolaitis, PG; Miller, RJ; Popa, L., Data exchange: semantics and query answering, Theor. Comput. Sci., 336, 1, 89-124 (2005) · Zbl 1080.68019 · doi:10.1016/j.tcs.2004.10.033 |
| [31] | Fitting, M., First-Order Logic and Automated Theorem Proving (1995), Berlin: Springer, Berlin · Zbl 0848.68101 |
| [32] | Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In: KR’92, pp. 425-435. Morgan Kaufmann (1992) |
| [33] | van Gelder, A.; Topor, RW, Safety and translation of relational calculus queries, ACM Trans. Database Syst., 16, 2, 235-278 (1991) · doi:10.1145/114325.103712 |
| [34] | Grau, BC; Horrocks, I.; Krötzsch, M.; Kupke, C.; Magka, D.; Motik, B.; Wang, Z., Acyclicity notions for existential rules and their application to query answering in ontologies, JAIR, 47, 741-808 (2013) · Zbl 1270.68295 · doi:10.1613/jair.3949 |
| [35] | Hoder, K., Holzer, A., Kovács, L., Voronkov, A.: Vinter: A Vampire-based tool for interpolation. In: APLAS 2012, LNCS, vol. 7705, pp. 148-156. Springer (2012) |
| [36] | Huang, G.: Constructing Craig interpolation formulas. In: COCOON ’95, LNCS, vol. 959, pp. 181-190. Springer (1995) · Zbl 1527.03007 |
| [37] | Hudek, A., Toman, D., Wedell, G.: On enumerating query plans using analytic tableau. In: TABLEAUX 2015, LNCS (LNAI), vol. 9323, pp. 339-354. Springer (2015) · Zbl 1471.68084 |
| [38] | Hähnle, R.; Robinson, A.; Voronkov, A., Tableaux and related methods, Handbook of Automatic Reasoning, chap. 3, 101-178 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 1011.68125 · doi:10.1016/B978-044450813-3/50005-9 |
| [39] | Jacobs, S.; Waldmann, U., Comparing instance generation methods for automated reasoning, J. Autom. Reason., 38, 1-3, 57-78 (2007) · Zbl 1113.68089 · doi:10.1007/s10817-006-9046-x |
| [40] | Järvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: TACAS 2010, LNCS, vol. 6015, pp. 129-144 (2010) · Zbl 1284.03208 |
| [41] | Kaliszyk, C.: Efficient low-level connection tableaux. In: TABLEAUX 2015, LNCS (LNAI), vol. 9323, pp. 102-111. Springer (2015) · Zbl 1471.68311 |
| [42] | Kaliszyk, C., Urban, J.: FEMaLeCoP: Fairly efficient machine learning connection prover. In: LPAR-20, LNCS, vol. 9450, pp. 88-96. Springer (2015) · Zbl 1471.68312 |
| [43] | Kiesl, B., Suda, M.: A unifying principle for clause elimination in first-order logic. In: CADE 26, LNCS (LNAI), vol. 10395, pp. 274-290. Springer (2017) · Zbl 1496.03048 |
| [44] | Kiesl, B., Suda, M., Seidl, M., Tompits, H., Biere, A.: Blocked clauses in first-order logic. In: LPAR-21, EPiC, vol. 46, pp. 31-48 (2017) · Zbl 1403.68240 |
| [45] | Kovács, L., Voronkov, A.: First-order interpolation and interpolating proof systems. In: LPAR-21, EPiC, vol. 46, pp. 49-64. EasyChair (2017) · Zbl 1402.03041 |
| [46] | Leone, N.; Pfeifer, G.; Faber, W.; Eiter, T.; Gottlob, G.; Perri, S.; Scarcello, F., The DLV system for knowledge representation and reasoning, ACM Trans. Comput. Log., 7, 3, 499-562 (2006) · Zbl 1367.68308 · doi:10.1145/1149114.1149117 |
| [47] | Letz, R.; Bibel, W.; Schmitt, PH, Clausal tableaux, Automated Deduction - A Basis for Applications, 43-72 (1998), Amsterdam: Kluwer Academic Publishers, Amsterdam · Zbl 0966.03013 |
| [48] | Letz, R.: First-order tableau methods. In: M. D’Agostino, D. M. Gabbay, R. Hähnle, J. Posegga (eds.) Handb. of Tableau Methods, pp. 125-196. Kluwer Academic Publishers (1999) · Zbl 0972.03524 |
| [49] | Letz, R.: Tableau and connection calculi. structure, complexity, implementation. Habilitationsschrift, TU München (1999). http://www2.tcs.ifi.lmu.de/ letz/habil.ps. Accessed 7 June 2020 |
| [50] | Letz, R.; Mayr, K.; Goller, C., Controlled integration of the cut rule into connection tableaux calculi, J. Autom. Reason., 13, 3, 297-337 (1994) · Zbl 0816.03005 · doi:10.1007/BF00881947 |
| [51] | Letz, R.; Schumann, J.; Bayerl, S.; Bibel, W., SETHEO: a high-performance theorem prover, J. Autom. Reason., 8, 2, 183-212 (1992) · Zbl 0759.68080 · doi:10.1007/BF00244282 |
| [52] | Letz, R.; Stenz, G.; Robinson, A.; Voronkov, A., Model elimination and connection tableau procedures, Handbook of Automatic Reasoning, 2015-2114 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 1011.68130 · doi:10.1016/B978-044450813-3/50030-8 |
| [53] | Loveland, DW, Automated Theorem Proving: A Logical Basis (1978), Amsterdam: North-Holland, Amsterdam · Zbl 0364.68082 |
| [54] | Lyndon, R., An interpolation theorem in the predicate calculus, Pac. J. Math., 9, 129-142 (1959) · Zbl 0093.01002 · doi:10.2140/pjm.1959.9.129 |
| [55] | Maier, D.; Mendelzon, AO; Sagiv, Y., Testing implications of data dependencies, ACM Trans. Database Syst., 4, 4, 455-469 (1979) · doi:10.1145/320107.320115 |
| [56] | Marx, M.: Queries determined by views: Pack your views. In: PODS ’07, pp. 23-30. ACM (2007) |
| [57] | McCune, W.: Prover9 and Mace4 (2005-2010). http://www.cs.unm.edu/ mccune/prover9 |
| [58] | McMillan, K.L.: Interpolation and SAT-based model checking. In: CAV 2003, LNCS, vol. 2725, pp. 1-13. Springer (2003) · Zbl 1278.68184 |
| [59] | McMillan, K.L.: Applications of Craig interpolants in model checking. In: TACAS 2005, LNCS, vol. 3440, pp. 1-12. Springer (2005) · Zbl 1087.68597 |
| [60] | McMillan, KL, An interpolating theorem prover, Theor. Comput. Sci., 345, 1, 101-121 (2005) · Zbl 1079.68092 · doi:10.1016/j.tcs.2005.07.003 |
| [61] | Moser, M.; Ibens, O.; Letz, R.; Steinbach, J.; Goller, C.; Schumann, J.; Mayr, K., SETHEO and E-SETHEO - the CADE-13 systems, J. Autom. Reason., 18, 2, 237-246 (1997) · doi:10.1023/A:1005808119103 |
| [62] | Motik, B.; Shearer, R.; Horrocks, I., Hypertableau reasoning for description logics, JAIR, 36, 165-228 (2009) · Zbl 1192.68664 · doi:10.1613/jair.2811 |
| [63] | Motohashi, N.: Equality and Lyndon’s interpolation theorem. J. Symb. Log. 49(1), 123-128 (1984) · Zbl 0574.03014 |
| [64] | Nash, A., Segoufin, L., Vianu, V.: Views and queries: Determinacy and rewriting. ACM Trans. Database Systems 35(3) (2010) |
| [65] | Oliver, B.E., Otten, J.: Equality preprocessing in connection calculi. In: PAAR-2020, CEUR Workshop Proceedings (2020) |
| [66] | Otten, J., Restricting backtracking in connection calculi, AI Commun., 23, 2-3, 159-182 (2010) · Zbl 1205.68363 · doi:10.3233/AIC-2010-0464 |
| [67] | Pelzer, B., Wernhard, C.: System description: E-KRHyper. In: CADE-21, LNCS (LNAI), vol. 4603, pp. 503-513. Springer (2007) · Zbl 1213.68574 |
| [68] | Plaisted, DA; Greenbaum, S., A structure-preserving clause form translation, J. Symb. Comput., 2, 293-304 (1986) · Zbl 0636.68119 · doi:10.1016/S0747-7171(86)80028-1 |
| [69] | Reckhow, R.A.: On the lengths of proofs in the propositional calculus. Ph.D. thesis, University of Toronto (1975). https://www.cs.toronto.edu/ sacook/homepage/reckhow_thesis.pdf. Accessed 7 June 2020 · Zbl 0375.02004 |
| [70] | Schulz, S., Cruanes, S., Vukmirovic, P.: Faster, higher, stronger: E 2.3. In: CADE 27, LNCS, vol. 11716, pp. 495-507. Springer (2019) · Zbl 1535.68460 |
| [71] | Scott, D., A decision method for validity of sentences in two variables, J. Symb. Log., 27, 4, 477 (1962) |
| [72] | Segoufin, L., Vianu, V.: Views and queries: determinacy and rewriting. In: PODS 2005, pp. 49-60. ACM (2005) |
| [73] | Smullyan, R.M.: First-Order Logic. Springer (1968). Also republished with corrections by Dover publications (1995) · Zbl 0172.28901 |
| [74] | Stickel, ME, A Prolog technology theorem prover: implementation by an extended Prolog compiler, J. Autom. Reason., 4, 4, 353-380 (1988) · Zbl 0662.68104 · doi:10.1007/BF00297245 |
| [75] | Tarski, A., Einige methologische Untersuchungen zur Definierbarkeit der Begriffe, Erkenntnis, 5, 80-100 (1935) · JFM 61.0050.03 · doi:10.1007/BF00172286 |
| [76] | Toman, D.; Weddell, G., Fundamentals of Physical Design and Query Compilation (2011), New York: Morgan & Claypool, New York · Zbl 1238.68004 · doi:10.2200/S00363ED1V01Y201105DTM018 |
| [77] | Toman, D., Weddell, G.: An interpolation-based compiler and optimizer for relational queries (system design report). In: IWIL 2017 Workshop and LPAR-21 Short Presentations, Kalpa, vol. 1. EasyChair (2017) |
| [78] | Tseitin, GS; Slisenko, AO, On the complexity of derivation in propositional calculus, Studies in Constructive Mathematics and Mathematical Logic, 115-125 (1970), London: Steklov Mathematical Institute, London · Zbl 0205.00402 |
| [79] | Wernhard, C.: System Description: KRHyper. Tech. Rep. Fachberichte Informatik 14-2003, Universität Koblenz-Landau, Koblenz, Germany (2003) · Zbl 1213.68574 |
| [80] | Wernhard, C.: Semantic knowledge partitioning. In: JELIA 04, LNAI, vol. 3229, pp. 552-564. Springer (2004) · Zbl 1111.68701 |
| [81] | Wernhard, C.: The PIE system for proving, interpolating and eliminating. In: PAAR-2016, CEUR Workshop Proceedings, vol. 1635, pp. 125-138 (2016) |
| [82] | Wernhard, C.: Craig interpolation and access interpolation with clausal first-order tableaux. CoRR abs/1802.04982 (2018). (Tech. rep. Technische Universität Dresden, KRR 18-01) |
| [83] | Wernhard, C.: Facets of the PIE environment for proving, interpolating and eliminating on the basis of first-order logic. In: DECLARE 2019, LNCS (LNAI), vol. 12057, pp. 160-177 (2020) |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
