{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:14Z","timestamp":1747592474242,"version":"3.40.3"},"publisher-location":"Cham","reference-count":64,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031435126"},{"type":"electronic","value":"9783031435133"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T00:00:00Z","timestamp":1694649600000},"content-version":"vor","delay-in-days":256,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/978-3-031-43513-3_1","type":"book-chapter","created":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T14:02:36Z","timestamp":1694613756000},"page":"3-23","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Range-Restricted and\u00a0Horn Interpolation through Clausal Tableaux"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0438-8829","authenticated-orcid":false,"given":"Christoph","family":"Wernhard","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,9,14]]},"reference":[{"key":"1_CR1","volume-title":"Foundations of Databases","author":"S Abiteboul","year":"1995","unstructured":"Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison Wesley, Boston (1995)"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-61630-6_1","volume-title":"Logics in Artificial Intelligence","author":"P Baumgartner","year":"1996","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper tableaux. In: Alferes, J.J., Pereira, L.M., Orlowska, E. (eds.) JELIA 1996. LNCS, vol. 1126, pp. 1\u201317. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61630-6_1"},{"key":"1_CR3","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/11814771_11","volume":"64","author":"P Baumgartner","year":"2020","unstructured":"Baumgartner, P., Schmidt, R.A.: Blocking and other enhancements for bottom-up model generation methods. J. Autom. Reasoning 64, 197\u2013251 (2020). https:\/\/doi.org\/10.1007\/11814771_11","journal-title":"J. Autom. Reasoning"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Benedikt, M., Kostylev, E.V., Mogavero, F., Tsamoura, E.: Reformulating queries: theory and practice. In: Sierra, C. (ed.) IJCAI 2017, pp. 837\u2013843. ijcai.org (2017). https:\/\/doi.org\/10.24963\/ijcai.2017\/116","DOI":"10.24963\/ijcai.2017\/116"},{"key":"1_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-01856-5","volume-title":"Generating Plans from Proofs: The Interpolation-based Approach to Query Reformulation","author":"M Benedikt","year":"2016","unstructured":"Benedikt, M., Leblay, J., ten Cate, B., Tsamoura, E.: Generating Plans from Proofs: The Interpolation-based Approach to Query Reformulation. Morgan & Claypool, San Rafael (2016). https:\/\/doi.org\/10.1007\/978-3-031-01856-5"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Benedikt, M., Pradic, C., Wernhard, C.: Synthesizing nested relational queries from implicit specifications. In: PODS \u201923, pp. 33\u201345 (2023). https:\/\/doi.org\/10.1145\/3584372.3588653","DOI":"10.1145\/3584372.3588653"},{"key":"1_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-322-90102-6","volume-title":"Automated Theorem Proving","author":"W Bibel","year":"1987","unstructured":"Bibel, W.: Automated Theorem Proving, 2nd edn. Vieweg, Braunschweig (1987). https:\/\/doi.org\/10.1007\/978-3-322-90102-6. First edition 1982","edition":"2"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-030-49424-7_13","volume-title":"The Legacy of Kurt Sch\u00fctte","author":"W Bibel","year":"2020","unstructured":"Bibel, W., Otten, J.: From Sch\u00fctte\u2019s formal systems to modern automated deduction. In: The Legacy of Kurt Sch\u00fctte, pp. 217\u2013251. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-49424-7_13"},{"issue":"1","key":"1_CR9","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10817-014-9314-0","volume":"54","author":"MP Bonacina","year":"2014","unstructured":"Bonacina, M.P., Johansson, M.: On interpolation in automated theorem proving. J. Autom. Reasoning 54(1), 69\u201397 (2014). https:\/\/doi.org\/10.1007\/s10817-014-9314-0","journal-title":"J. Autom. Reasoning"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-18275-4_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Brillout","year":"2011","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: Beyond quantifier-free interpolation in extensions of Presburger arithmetic. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 88\u2013102. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_8"},{"issue":"1","key":"1_CR11","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1023\/A:1006291616338","volume":"25","author":"F Bry","year":"2000","unstructured":"Bry, F., Yahya, A.H.: Positive unit hyperresolution tableaux and their application to minimal model generation. J. Autom. Reasoning 25(1), 35\u201382 (2000). https:\/\/doi.org\/10.1023\/A:1006291616338","journal-title":"J. Autom. Reasoning"},{"key":"1_CR12","volume-title":"Symbolic Logic and Automated Theorem Proving","author":"CL Chang","year":"1973","unstructured":"Chang, C.L., Lee, R.C.T.: Symbolic Logic and Automated Theorem Proving. Academic Press, Cambridge (1973)"},{"issue":"3","key":"1_CR13","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250\u2013268 (1957). https:\/\/doi.org\/10.2307\/2963593","journal-title":"J. Symb. Log."},{"issue":"3","key":"1_CR14","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3), 269\u2013285 (1957). https:\/\/doi.org\/10.2307\/2963594","journal-title":"J. Symb. Log."},{"issue":"3","key":"1_CR15","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s11229-008-9353-3","volume":"164","author":"W Craig","year":"2008","unstructured":"Craig, W.: The road to two theorems of logic. Synthese 164(3), 333\u2013339 (2008). https:\/\/doi.org\/10.1007\/s11229-008-9353-3","journal-title":"Synthese"},{"key":"1_CR16","unstructured":"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\u201997, pp. 58\u201362. RISC-Linz Report Series No. 97\u201350, Joh. Kepler Univ., Linz (1997). https:\/\/www.logic.at\/ftp97\/papers\/dahn.pdf"},{"key":"1_CR17","unstructured":"Demolombe, R.: Syntactical characterization of a subset of domain independent formulas. Technical report, ONERA-CERT, Toulouse (1982)"},{"key":"1_CR18","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1145\/147508.147520","volume":"39","author":"R Demolombe","year":"1992","unstructured":"Demolombe, R.: Syntactical characterization of a subset of domain independent formulas. JACM 39, 71\u201394 (1992). https:\/\/doi.org\/10.1145\/147508.147520","journal-title":"JACM"},{"key":"1_CR19","unstructured":"Eder, E.: An implementation of a theorem prover based on the connection method. In: Bibel, W., Petkoff, B. (eds.) AIMSA\u201984, pp. 121\u2013128. North-Holland (1985)"},{"key":"1_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M Fitting","year":"1995","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Cham (1995). https:\/\/doi.org\/10.1007\/978-1-4612-2360-3","edition":"2"},{"key":"1_CR21","doi-asserted-by":"publisher","first-page":"885","DOI":"10.1613\/jair.4058","volume":"48","author":"E Franconi","year":"2013","unstructured":"Franconi, E., Kerhet, V., Ngo, N.: Exact query reformulation over databases with first-order and description logics ontologies. JAIR 48, 885\u2013922 (2013). https:\/\/doi.org\/10.1613\/jair.4058","journal-title":"JAIR"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-35182-2_11","volume-title":"Programming Languages and Systems","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Holzer, A., Kov\u00e1cs, L., Voronkov, A.: Vinter: a Vampire-based tool for interpolation. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 148\u2013156. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35182-2_11"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-14203-1_16","volume-title":"Automated Reasoning","author":"K Hoder","year":"2010","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination in Vampire. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 188\u2013195. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_16"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/BFb0030832","volume-title":"Computing and Combinatorics","author":"G Huang","year":"1995","unstructured":"Huang, G.: Constructing Craig interpolation formulas. In: Du, D.-Z., Li, M. (eds.) COCOON 1995. LNCS, vol. 959, pp. 181\u2013190. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0030832"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-319-24312-2_23","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A Hudek","year":"2015","unstructured":"Hudek, A., Toman, D., Weddell, G.: On enumerating query plans using analytic tableau. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 339\u2013354. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24312-2_23"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, chap. 3, pp. 101\u2013178. Elsevier (2001). https:\/\/doi.org\/10.1016\/b978-044450813-3\/50005-9","DOI":"10.1016\/b978-044450813-3\/50005-9"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order interpolation and interpolating proof systems. In: Eiter, T., Sands, D. (eds.) LPAR-21. EPiC, vol.\u00a046, pp. 49\u201364. EasyChair (2017). https:\/\/doi.org\/10.29007\/1qb8","DOI":"10.29007\/1qb8"},{"key":"1_CR29","unstructured":"Letz, R.: Clausal tableaux. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction - A Basis for Applications, vol. I, pp. 43\u201372. Kluwer Academic Publishers (1998)"},{"key":"1_CR30","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-94-017-1754-0_3","volume-title":"Handbook of Tableau Methods","author":"R Letz","year":"1999","unstructured":"Letz, R.: First-order tableau methods. In: D\u2019Agostino, A., Gabbay, D.M., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 125\u2013196. Springer, Dordrecht (1999)"},{"key":"1_CR31","unstructured":"Letz, R.: Tableau and Connection Calculi. Structure, Complexity, Implementation. Habilitationsschrift, TU M\u00fcnchen (1999). http:\/\/www2.tcs.ifi.lmu.de\/~letz\/habil.pdf. Accessed 19 July 2023"},{"issue":"2","key":"1_CR32","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO: a high-performance theorem prover. J. Autom. Reasoning 8(2), 183\u2013212 (1992). https:\/\/doi.org\/10.1007\/BF00244282","journal-title":"J. Autom. Reasoning"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 2015\u20132114. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50030-8"},{"key":"1_CR34","volume-title":"Automated Theorem Proving: A Logical Basis","author":"DW Loveland","year":"1978","unstructured":"Loveland, D.W.: Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam (1978)"},{"key":"1_CR35","doi-asserted-by":"publisher","first-page":"129","DOI":"10.2140\/pjm.1959.9.129","volume":"9","author":"R Lyndon","year":"1959","unstructured":"Lyndon, R.: An interpolation theorem in the predicate calculus. Pac. J. Math. 9, 129\u2013142 (1959). https:\/\/doi.org\/10.2140\/pjm.1959.9.129","journal-title":"Pac. J. Math."},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"9th International Conference on Automated Deduction","author":"R Manthey","year":"1988","unstructured":"Manthey, R., Bry, F.: SATCHMO: A theorem prover implemented in Prolog. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 415\u2013434. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/BFb0012847"},{"key":"1_CR37","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). http:\/\/www.cs.unm.edu\/~mccune\/prover9. Accessed 19 July 2023"},{"issue":"2","key":"1_CR38","doi-asserted-by":"publisher","first-page":"221","DOI":"10.2307\/2272123","volume":"42","author":"GF McNulty","year":"1977","unstructured":"McNulty, G.F.: Fragments of first order logic, I: universal Horn logic. J. Symb. Log. 42(2), 221\u2013237 (1977). https:\/\/doi.org\/10.2307\/2272123","journal-title":"J. Symb. Log."},{"issue":"3","key":"1_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1806907.1806913","volume":"35","author":"A Nash","year":"2010","unstructured":"Nash, A., Segoufin, L., Vianu, V.: Views and queries: determinacy and rewriting. ACM Trans. Database Syst. 35(3), 1\u201341 (2010). https:\/\/doi.org\/10.1145\/1806907.1806913","journal-title":"ACM Trans. Database Syst."},{"key":"1_CR40","unstructured":"Nicolas, J.M.: Logics for improving integrity checking in relational data bases. Technical report, ONERA-CERT, Toulouse (1979)"},{"issue":"3","key":"1_CR41","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/BF00263192","volume":"18","author":"JM Nicolas","year":"1982","unstructured":"Nicolas, J.M.: Logics for improving integrity checking in relational data bases. Acta Informatica 18(3), 227\u2013253 (1982). https:\/\/doi.org\/10.1007\/BF00263192","journal-title":"Acta Informatica"},{"issue":"2\u20133","key":"1_CR42","doi-asserted-by":"publisher","first-page":"159","DOI":"10.3233\/AIC-2010-0464","volume":"23","author":"J Otten","year":"2010","unstructured":"Otten, J.: Restricting backtracking in connection calculi. AI Commun. 23(2\u20133), 159\u2013182 (2010). https:\/\/doi.org\/10.3233\/AIC-2010-0464","journal-title":"AI Commun."},{"issue":"1\u20132","key":"1_CR43","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0747-7171(03)00037-3","volume":"36","author":"J Otten","year":"2003","unstructured":"Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36(1\u20132), 139\u2013161 (2003). https:\/\/doi.org\/10.1016\/S0747-7171(03)00037-3","journal-title":"J. Symb. Comput."},{"key":"1_CR44","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2, 293\u2013304 (1986). https:\/\/doi.org\/10.1016\/S0747-7171(86)80028-1","journal-title":"J. Symb. Comput."},{"key":"1_CR45","doi-asserted-by":"publisher","unstructured":"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\u2013174. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-43513-3_9","DOI":"10.1007\/978-3-031-43513-3_9"},{"issue":"3","key":"1_CR46","first-page":"227","volume":"1","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1(3), 227\u2013234 (1965)","journal-title":"Int. J. Comput. Math."},{"key":"1_CR47","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274\u2013289. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_20"},{"key":"1_CR48","unstructured":"Schulz, S.: Credo Quia absurdum (?) \u2013 proof generation and challenges of proof generation. In: PAMLTP\/DG4D$$^3$$ (2023), workshop presentation. https:\/\/europroofnet.github.io\/_pages\/WG5\/Prague23\/pres\/Schulz.pdf"},{"key":"1_CR49","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-030-29436-6_29","volume-title":"Automated Deduction \u2013 CADE 27","author":"S Schulz","year":"2019","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 495\u2013507. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29"},{"issue":"4","key":"1_CR50","first-page":"477","volume":"27","author":"D Scott","year":"1962","unstructured":"Scott, D.: A decision method for validity of sentences in two variables. J. Symb. Log. 27(4), 477 (1962)","journal-title":"J. Symb. Log."},{"issue":"4","key":"1_CR51","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"JR Slagle","year":"1967","unstructured":"Slagle, J.R.: Automatic theorem proving with renamable and semantic resolution. JACM 14(4), 687\u2013697 (1967). https:\/\/doi.org\/10.1145\/321420.321428","journal-title":"JACM"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"Smullyan, R.M.: First-Order Logic. Springer, New York (1968). also republished with corrections by Dover publications (1995)","DOI":"10.1007\/978-3-642-86718-7"},{"issue":"4","key":"1_CR53","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"ME Stickel","year":"1988","unstructured":"Stickel, M.E.: A Prolog technology theorem prover: implementation by an extended Prolog compiler. J. Autom. Reasoning 4(4), 353\u2013380 (1988). https:\/\/doi.org\/10.1007\/BF00297245","journal-title":"J. Autom. Reasoning"},{"key":"1_CR54","doi-asserted-by":"publisher","DOI":"10.3233\/AIC-220244","author":"G Sutcliffe","year":"2023","unstructured":"Sutcliffe, G., Desharnais, M.: The 11th IJCAR automated theorem proving system competition - CASC-J11. AI Commun. (2023). https:\/\/doi.org\/10.3233\/AIC-220244","journal-title":"AI Commun."},{"key":"1_CR55","unstructured":"Takeuti, G.: Proof Theory, second edn. North-Holland (1987)"},{"key":"1_CR56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-01881-7","volume-title":"Fundamentals of Physical Design and Query Compilation","author":"D Toman","year":"2011","unstructured":"Toman, D., Weddell, G.: Fundamentals of Physical Design and Query Compilation. Morgan & Claypool, San Rafael (2011). https:\/\/doi.org\/10.1007\/978-3-031-01881-7"},{"key":"1_CR57","doi-asserted-by":"publisher","unstructured":"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.\u00a01. EasyChair (2017). https:\/\/doi.org\/10.29007\/53fk","DOI":"10.29007\/53fk"},{"key":"1_CR58","doi-asserted-by":"crossref","unstructured":"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\u2013125. Steklov Mathematical Institute (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"issue":"2","key":"1_CR59","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1145\/114325.103712","volume":"16","author":"A Van Gelder","year":"1991","unstructured":"Van Gelder, A., Topor, R.W.: Safety and translation of relational calculus queries. ACM Trans. Database Syst. 16(2), 235\u2013278 (1991). https:\/\/doi.org\/10.1145\/114325.103712","journal-title":"ACM Trans. Database Syst."},{"key":"1_CR60","unstructured":"Wernhard, C.: The PIE system for proving, interpolating and eliminating. In: Fontaine, P., Schulz, S., Urban, J. (eds.) PAAR\u00a02016. CEUR Workshop Proc., vol.\u00a01635, pp. 125\u2013138. CEUR-WS.org (2016). http:\/\/ceur-ws.org\/Vol-1635\/paper-11.pdf"},{"key":"1_CR61","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-030-46714-2_11","volume-title":"Declarative Programming and Knowledge Management","author":"C Wernhard","year":"2020","unstructured":"Wernhard, C.: Facets of the PIE environment for proving, interpolating and eliminating on the basis of first-order logic. In: Hofstedt, P., Abreu, S., John, U., Kuchen, H., Seipel, D. (eds.) INAP\/WLP\/WFLP -2019. LNCS (LNAI), vol. 12057, pp. 160\u2013177. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-46714-2_11"},{"issue":"5","key":"1_CR62","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/s10817-021-09590-3","volume":"65","author":"C Wernhard","year":"2021","unstructured":"Wernhard, C.: Craig interpolation with clausal first-order tableaux. J. Autom. Reasoning 65(5), 647\u2013690 (2021). https:\/\/doi.org\/10.1007\/s10817-021-09590-3","journal-title":"J. Autom. Reasoning"},{"key":"1_CR63","doi-asserted-by":"publisher","unstructured":"Wernhard, C.: Range-restricted and Horn interpolation through clausal tableaux. CoRR abs\/2306.03572 (2023). https:\/\/doi.org\/10.48550\/arXiv.2306.03572","DOI":"10.48550\/arXiv.2306.03572"},{"key":"1_CR64","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-030-79876-5_4","volume-title":"Automated Deduction \u2013 CADE 28","author":"C Wernhard","year":"2021","unstructured":"Wernhard, C., Bibel, W.: Learning from \u0141ukasiewicz and Meredith: investigations into proof structures. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 58\u201375. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_4"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-43513-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T14:03:09Z","timestamp":1694613789000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43513-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031435126","9783031435133"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43513-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"14 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/tableaux2023.tableaux-ar.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"47% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3 (2.92)","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}