Range-restricted and Horn interpolation through clausal tableaux. (English) Zbl 07850735
Ramanayake, Revantha (ed.) et al., Automated reasoning with analytic tableaux and related methods. 32nd international conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14278, 3-23 (2023).
Summary: We show how variations of range-restriction and also the Horn property can be passed from inputs to outputs of Craig interpolation in first-order logic. The proof system is clausal tableaux, which stems from first-order ATP. Our results are induced by a restriction of the clausal tableau structure, which can be achieved in general by a proof transformation, also if the source proof is by resolution/paramodulation. Primarily addressed applications are query synthesis and reformulation with interpolation. Our methodical approach combines operations on proof structures with the immediate perspective of feasible implementation through incorporating highly optimized first-order provers.
For the entire collection see [Zbl 1537.68012].
For the entire collection see [Zbl 1537.68012].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Abiteboul, S.; Hull, R.; Vianu, V., Foundations of Databases (1995), Boston: Addison Wesley, Boston · Zbl 0848.68031 |
| [2] | Baumgartner, P.; Furbach, U.; Niemelä, I.; Alferes, JJ; Pereira, LM; Orlowska, E., Hyper tableaux, Logics in Artificial Intelligence, 1-17 (1996), Heidelberg: Springer, Heidelberg · Zbl 1427.03031 · doi:10.1007/3-540-61630-6_1 |
| [3] | Baumgartner, P.; Schmidt, RA, Blocking and other enhancements for bottom-up model generation methods, J. Autom. Reasoning, 64, 197-251 (2020) · Zbl 1468.68279 · doi:10.1007/11814771_11 |
| [4] | Benedikt, M., Kostylev, E.V., Mogavero, F., Tsamoura, E.: Reformulating queries: theory and practice. In: Sierra, C. (ed.) IJCAI 2017, pp. 837-843. ijcai.org (2017). doi:10.24963/ijcai.2017/116 |
| [5] | Benedikt, M.; Leblay, J.; ten Cate, B.; Tsamoura, E., Generating Plans from Proofs: The Interpolation-based Approach to Query Reformulation (2016), San Rafael: Morgan & Claypool, San Rafael · Zbl 1345.68003 · doi:10.1007/978-3-031-01856-5 |
| [6] | Benedikt, M., Pradic, C., Wernhard, C.: Synthesizing nested relational queries from implicit specifications. In: PODS ’23, pp. 33-45 (2023). doi:10.1145/3584372.3588653 |
| [7] | Bibel, W., Automated Theorem Proving (1987), Braunschweig: Vieweg, Braunschweig · Zbl 0639.68092 · doi:10.1007/978-3-322-90102-6 |
| [8] | Bibel, W.; Otten, J., From Schütte’s formal systems to modern automated deduction, The Legacy of Kurt Schütte, 217-251 (2020), Cham: Springer, Cham · Zbl 1535.03001 · doi:10.1007/978-3-030-49424-7_13 |
| [9] | Bonacina, MP; Johansson, M., On interpolation in automated theorem proving, J. Autom. Reasoning, 54, 1, 69-97 (2014) · Zbl 1315.03018 · doi:10.1007/s10817-014-9314-0 |
| [10] | Brillout, A.; Kroening, D.; Rümmer, P.; Wahl, T.; Jhala, R.; Schmidt, D., Beyond quantifier-free interpolation in extensions of Presburger arithmetic, Verification, Model Checking, and Abstract Interpretation, 88-102 (2011), Heidelberg: Springer, Heidelberg · Zbl 1318.03045 · doi:10.1007/978-3-642-18275-4_8 |
| [11] | Bry, F.; Yahya, AH, Positive unit hyperresolution tableaux and their application to minimal model generation, J. Autom. Reasoning, 25, 1, 35-82 (2000) · Zbl 0960.03006 · doi:10.1023/A:1006291616338 |
| [12] | Chang, CL; Lee, RCT, Symbolic Logic and Automated Theorem Proving (1973), Cambridge: Academic Press, Cambridge · Zbl 0263.68046 |
| [13] | 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 |
| [14] | 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 |
| [15] | 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 |
| [16] | Dahn, I., Wernhard, C.: First order proof problems extracted from an article in the Mizar mathematical library. In: Bonacina, M.P., Furbach, U. (eds.) FTP’97, pp. 58-62. RISC-Linz Report Series No. 97-50, Joh. Kepler Univ., Linz (1997). https://www.logic.at/ftp97/papers/dahn.pdf |
| [17] | Demolombe, R.: Syntactical characterization of a subset of domain independent formulas. Technical report, ONERA-CERT, Toulouse (1982) · Zbl 0799.68061 |
| [18] | Demolombe, R., Syntactical characterization of a subset of domain independent formulas, JACM, 39, 71-94 (1992) · Zbl 0799.68061 · doi:10.1145/147508.147520 |
| [19] | Eder, E.: An implementation of a theorem prover based on the connection method. In: Bibel, W., Petkoff, B. (eds.) AIMSA’84, pp. 121-128. North-Holland (1985) |
| [20] | Fitting, M., First-Order Logic and Automated Theorem Proving (1995), Cham: Springer, Cham · Zbl 0848.68101 · doi:10.1007/978-1-4612-2360-3 |
| [21] | Franconi, E.; Kerhet, V.; Ngo, N., Exact query reformulation over databases with first-order and description logics ontologies, JAIR, 48, 885-922 (2013) · Zbl 1314.68118 · doi:10.1613/jair.4058 |
| [22] | Hoder, K.; Holzer, A.; Kovács, L.; Voronkov, A.; Jhala, R.; Igarashi, A., Vinter: a Vampire-based tool for interpolation, Programming Languages and Systems, 148-156 (2012), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-35182-2_11 |
| [23] | Hoder, K.; Kovács, L.; Voronkov, A.; Giesl, J.; Hähnle, R., Interpolation and symbol elimination in Vampire, Automated Reasoning, 188-195 (2010), Heidelberg: Springer, Heidelberg · Zbl 1291.68348 · doi:10.1007/978-3-642-14203-1_16 |
| [24] | Huang, G.; Du, D-Z; Li, M., Constructing Craig interpolation formulas, Computing and Combinatorics, 181-190 (1995), Heidelberg: Springer, Heidelberg · Zbl 1527.03007 · doi:10.1007/BFb0030832 |
| [25] | Hudek, A.; Toman, D.; Weddell, G.; De Nivelle, H., On enumerating query plans using analytic tableau, Automated Reasoning with Analytic Tableaux and Related Methods, 339-354 (2015), Cham: Springer, Cham · Zbl 1471.68084 · doi:10.1007/978-3-319-24312-2_23 |
| [26] | Hähnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, chap. 3, pp. 101-178. Elsevier (2001). doi:10.1016/b978-044450813-3/50005-9 · Zbl 1011.68125 |
| [27] | Kovács, L.; Voronkov, A.; Sharygina, N.; Veith, H., First-order theorem proving and Vampire, Computer Aided Verification, 1-35 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-39799-8_1 |
| [28] | Kovács, L., Voronkov, A.: First-order interpolation and interpolating proof systems. In: Eiter, T., Sands, D. (eds.) LPAR-21. EPiC, vol. 46, pp. 49-64. EasyChair (2017). doi:10.29007/1qb8 · Zbl 1402.03041 |
| [29] | Letz, R.: Clausal tableaux. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction - A Basis for Applications, vol. I, pp. 43-72. Kluwer Academic Publishers (1998) · Zbl 0966.03013 |
| [30] | Letz, R.; D’Agostino, A.; Gabbay, DM; Hähnle, R.; Posegga, J., First-order tableau methods, Handbook of Tableau Methods, 125-196 (1999), Dordrecht: Springer, Dordrecht · Zbl 0972.03524 · doi:10.1007/978-94-017-1754-0_3 |
| [31] | Letz, R.: Tableau and Connection Calculi. Structure, Complexity, Implementation. Habilitationsschrift, TU München (1999). http://www2.tcs.ifi.lmu.de/ letz/habil.pdf. Accessed 19 July 2023 |
| [32] | Letz, R.; Schumann, J.; Bayerl, S.; Bibel, W., SETHEO: a high-performance theorem prover, J. Autom. Reasoning, 8, 2, 183-212 (1992) · Zbl 0759.68080 · doi:10.1007/BF00244282 |
| [33] | Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 2015-2114. Elsevier (2001) · Zbl 1011.68130 |
| [34] | Loveland, DW, Automated Theorem Proving: A Logical Basis (1978), Amsterdam: North-Holland, Amsterdam · Zbl 0364.68082 |
| [35] | 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 |
| [36] | Manthey, R.; Bry, F.; Lusk, E.; Overbeek, R., SATCHMO: A theorem prover implemented in Prolog, 9th International Conference on Automated Deduction, 415-434 (1988), Heidelberg: Springer, Heidelberg · Zbl 0668.68104 · doi:10.1007/BFb0012847 |
| [37] | McCune, W.: Prover9 and Mace4 (2005-2010). http://www.cs.unm.edu/ mccune/prover9. Accessed 19 July 2023 |
| [38] | McNulty, GF, Fragments of first order logic, I: universal Horn logic, J. Symb. Log., 42, 2, 221-237 (1977) · Zbl 0381.03011 · doi:10.2307/2272123 |
| [39] | Nash, A.; Segoufin, L.; Vianu, V., Views and queries: determinacy and rewriting, ACM Trans. Database Syst., 35, 3, 1-41 (2010) · doi:10.1145/1806907.1806913 |
| [40] | Nicolas, J.M.: Logics for improving integrity checking in relational data bases. Technical report, ONERA-CERT, Toulouse (1979) |
| [41] | Nicolas, JM, Logics for improving integrity checking in relational data bases, Acta Informatica, 18, 3, 227-253 (1982) · Zbl 0478.68096 · doi:10.1007/BF00263192 |
| [42] | Otten, J., Restricting backtracking in connection calculi, AI Commun., 23, 2-3, 159-182 (2010) · Zbl 1205.68363 · doi:10.3233/AIC-2010-0464 |
| [43] | Otten, J.; Bibel, W., leanCoP: lean connection-based theorem proving, J. Symb. Comput., 36, 1-2, 139-161 (2003) · Zbl 1025.68076 · doi:10.1016/S0747-7171(03)00037-3 |
| [44] | 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 |
| [45] | Rawson, M., Wernhard, C., Zombori, Z., Bibel, W.: Lemmas: generation, selection, application. In: Ramanayake, R., Urban, J. (eds.) TABLEAUX 2023. LNCS (LNAI), vol. 14278, pp. 153-174. Springer, Heidelberg (2023). doi:10.1007/978-3-031-43513-3_9 · Zbl 07850743 |
| [46] | Robinson, JA, Automatic deduction with hyper-resolution, Int. J. Comput. Math., 1, 3, 227-234 (1965) · Zbl 0158.26003 |
| [47] | Rümmer, P.; Cervesato, I.; Veith, H.; Voronkov, A., A constraint sequent calculus for first-order logic with linear integer arithmetic, Logic for Programming, Artificial Intelligence, and Reasoning, 274-289 (2008), Heidelberg: Springer, Heidelberg · Zbl 1182.03035 · doi:10.1007/978-3-540-89439-1_20 |
| [48] | Schulz, S.: Credo Quia absurdum (?) - proof generation and challenges of proof generation. In: PAMLTP/\(DG4D^3 (2023)\), workshop presentation. https://europroofnet.github.io/_pages/WG5/Prague23/pres/Schulz.pdf |
| [49] | Schulz, S.; Cruanes, S.; Vukmirović, P.; Fontaine, P., Faster, higher, stronger: E 2.3, Automated Deduction - CADE 27, 495-507 (2019), Cham: Springer, Cham · Zbl 1535.68460 · doi:10.1007/978-3-030-29436-6_29 |
| [50] | Scott, D., A decision method for validity of sentences in two variables, J. Symb. Log., 27, 4, 477 (1962) |
| [51] | Slagle, JR, Automatic theorem proving with renamable and semantic resolution, JACM, 14, 4, 687-697 (1967) · Zbl 0157.02405 · doi:10.1145/321420.321428 |
| [52] | Smullyan, R.M.: First-Order Logic. Springer, New York (1968). also republished with corrections by Dover publications (1995) · Zbl 0172.28901 |
| [53] | Stickel, ME, A Prolog technology theorem prover: implementation by an extended Prolog compiler, J. Autom. Reasoning, 4, 4, 353-380 (1988) · Zbl 0662.68104 · doi:10.1007/BF00297245 |
| [54] | Sutcliffe, G.; Desharnais, M., The 11th IJCAR automated theorem proving system competition - CASC-J11, AI Commun. (2023) · Zbl 1532.68123 · doi:10.3233/AIC-220244 |
| [55] | Takeuti, G.: Proof Theory, second edn. North-Holland (1987) · Zbl 0609.03019 |
| [56] | Toman, D.; Weddell, G., Fundamentals of Physical Design and Query Compilation (2011), San Rafael: Morgan & Claypool, San Rafael · Zbl 1238.68004 · doi:10.1007/978-3-031-01881-7 |
| [57] | Toman, D., Weddell, G.: An interpolation-based compiler and optimizer for relational queries (system design report). In: Eiter, T., Sands, D., Sutcliffe, G., Voronkov, A. (eds.) IWIL 2017 Workshop and LPAR-21 Short Presentations. Kalpa, vol. 1. EasyChair (2017). doi:10.29007/53fk |
| [58] | Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, vol. Part II, pp. 115-125. Steklov Mathematical Institute (1970) · Zbl 0205.00402 |
| [59] | 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 |
| [60] | Wernhard, C.: The PIE system for proving, interpolating and eliminating. In: Fontaine, P., Schulz, S., Urban, J. (eds.) PAAR 2016. CEUR Workshop Proc., vol. 1635, pp. 125-138. CEUR-WS.org (2016). http://ceur-ws.org/Vol-1635/paper-11.pdf |
| [61] | Wernhard, C.; Hofstedt, P.; Abreu, S.; John, U.; Kuchen, H.; Seipel, D., Facets of the PIE environment for proving, interpolating and eliminating on the basis of first-order logic, Declarative Programming and Knowledge Management, 160-177 (2020), Cham: Springer, Cham · doi:10.1007/978-3-030-46714-2_11 |
| [62] | Wernhard, C., Craig interpolation with clausal first-order tableaux, J. Autom. Reasoning, 65, 5, 647-690 (2021) · Zbl 1543.03053 · doi:10.1007/s10817-021-09590-3 |
| [63] | Wernhard, C.: Range-restricted and Horn interpolation through clausal tableaux. CoRR abs/2306.03572 (2023). doi:10.48550/arXiv.2306.03572 |
| [64] | Wernhard, C.; Bibel, W.; Platzer, A.; Sutcliffe, G., Learning from Łukasiewicz and Meredith: investigations into proof structures, Automated Deduction - CADE 28, 58-75 (2021), Cham: Springer, Cham · Zbl 1540.03028 · doi:10.1007/978-3-030-79876-5_4 |
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.
