{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:17Z","timestamp":1747592477303,"version":"3.37.3"},"reference-count":83,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2021,5,27]],"date-time":"2021-05-27T00:00:00Z","timestamp":1622073600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,5,27]],"date-time":"2021-05-27T00:00:00Z","timestamp":1622073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["WE 5641\/1-1"],"award-info":[{"award-number":["WE 5641\/1-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,6]]},"DOI":"10.1007\/s10817-021-09590-3","type":"journal-article","created":{"date-parts":[[2021,5,27]],"date-time":"2021-05-27T06:02:37Z","timestamp":1622095357000},"page":"647-690","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Craig Interpolation with Clausal First-Order Tableaux"],"prefix":"10.1007","volume":"65","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":[[2021,5,27]]},"reference":[{"key":"9590_CR1","volume-title":"Methods of Cut-Elimination","author":"M Baaz","year":"2011","unstructured":"Baaz, M., Leitsch, A.: Methods of Cut-Elimination. Springer, Berlin (2011)"},{"key":"9590_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H., Voronkov, A.: Elimination of equality via transformation with ordering constraints. In: CADE-15, LNCS (LNAI), vol. 1421, pp. 175\u2013190. Springer (1998)","DOI":"10.1007\/BFb0054259"},{"key":"9590_CR3","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper tableaux. In: JELIA\u201996, LNCS (LNAI), vol. 1126, pp. 1\u201317. Springer (1996)","DOI":"10.1007\/3-540-61630-6_1"},{"key":"9590_CR4","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/s10817-019-09515-1","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. Reason. 64, 197\u2013251 (2020)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9590_CR5","first-page":"35","volume":"24","author":"P Baumgartner","year":"2010","unstructured":"Baumgartner, P., Thorstensen, E.: Instance based methods \u2013 a brief overview. KI 24(1), 35\u201342 (2010)","journal-title":"KI"},{"key":"9590_CR6","doi-asserted-by":"crossref","unstructured":"Bender, M., Pelzer, B., Schon, C.: System description: E-KRHyper 1.4. In: CADE-24, LNCS (LNAI), vol. 7898, pp. 126\u2013134. Springer (2013)","DOI":"10.1007\/978-3-642-38574-2_8"},{"key":"9590_CR7","doi-asserted-by":"crossref","unstructured":"Benedikt, M., ten Cate, B., Tsamoura, E.: Generating low-cost plans from proofs. In: PODS\u201914, pp. 200\u2013211. ACM (2014)","DOI":"10.1145\/2594538.2594550"},{"key":"9590_CR8","doi-asserted-by":"crossref","unstructured":"Benedikt, M., Kostylev, E.V., Mogavero, F., Tsamoura, E.: Reformulating queries: theory and practice. In: IJCAI 2017, pp. 837\u2013843 (2017)","DOI":"10.24963\/ijcai.2017\/116"},{"key":"9590_CR9","doi-asserted-by":"publisher","DOI":"10.1145\/2847523","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, New York (2016)"},{"key":"9590_CR10","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated Theorem Proving. Vieweg (1982). Second edition 1987","DOI":"10.1007\/978-3-322-90100-2"},{"key":"9590_CR11","doi-asserted-by":"crossref","unstructured":"Bibel, W., Otten, J.: From Sch\u00fctte\u2019s formal systems to modern automated deduction. In: Kahle, R., Rathjen, M. (eds.) The Legacy of Kurt Sch\u00fctte, chap.\u00a013, pp. 215\u2013249. Springer (2020)","DOI":"10.1007\/978-3-030-49424-7_13"},{"key":"9590_CR12","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Johansson, M.: On interpolation in decision procedures. In: TABLEAUX 2011, LNCS (LNAI), vol. 6793, pp. 1\u201316. Springer (2012)","DOI":"10.1007\/978-3-642-22119-4_1"},{"issue":"4","key":"9590_CR13","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/s10817-015-9325-5","volume":"54","author":"MP Bonacina","year":"2015","unstructured":"Bonacina, M.P., Johansson, M.: Interpolation systems for ground proofs in automated deduction: a survey. J. Autom. Reason. 54(4), 353\u2013390 (2015)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9590_CR14","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10817-014-9314-0","volume":"54","author":"MP Bonacina","year":"2015","unstructured":"Bonacina, M.P., Johansson, M.: On interpolation in automated theorem proving. J. Autom. Reason. 54(1), 69\u201397 (2015)","journal-title":"J. Autom. Reason."},{"key":"9590_CR15","unstructured":"Borgida, A., de\u00a0Bruijn, J., Franconi, E., Seylan, I., Straccia, U., Toman, D., Weddell, G.: On finding query rewritings under expressive constraints. In: SEBD 2010. Esculapio Editore (2010)"},{"issue":"4","key":"9590_CR16","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D Brand","year":"1975","unstructured":"Brand, D.: Proving theorems with the modification method. SIAM J. Comput. 4(4), 412\u2013430 (1975)","journal-title":"SIAM J. Comput."},{"issue":"4","key":"9590_CR17","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s10817-011-9237-y","volume":"47","author":"A Brillout","year":"2011","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. J. Autom. Reason. 47(4), 341\u2013367 (2011)","journal-title":"J. Autom. Reason."},{"key":"9590_CR18","doi-asserted-by":"crossref","unstructured":"Bry, F., Manthey, R.: SATCHMO: A theorem prover implemented in Prolog. In: CADE-9, LNCS, vol. 310, pp. 415\u2013434. Springer (1988)","DOI":"10.1007\/BFb0012847"},{"key":"9590_CR19","doi-asserted-by":"crossref","unstructured":"B\u00e1r\u00e1ny, V., Benedikt, M., ten Cate, B.: Rewriting guarded negation queries. In: MFCS 2013, LNCS, vol. 8087, pp. 98\u2013110. Springer (2013)","DOI":"10.1007\/978-3-642-40313-2_11"},{"key":"9590_CR20","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)"},{"key":"9590_CR21","unstructured":"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\u00fcr Informatik (2010)"},{"key":"9590_CR22","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: TACAS\u00a02013, LNCS, vol. 7795, pp. 93\u2013107. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"issue":"3","key":"9590_CR23","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)","journal-title":"J. Symb. Log."},{"issue":"3","key":"9590_CR24","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)","journal-title":"J. Symb. Log."},{"issue":"3","key":"9590_CR25","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)","journal-title":"Synthese"},{"key":"9590_CR26","unstructured":"Dahn, I., Wernhard, C.: First order proof problems extracted from an article in the Mizar mathematical library. In: FTP\u201997, RISC-Linz Report Series No. 97\u201350, pp. 58\u201362. Joh. Kepler Univ., Linz, Austria (1997)"},{"key":"9590_CR27","first-page":"162","volume":"43","author":"N Dershowitz","year":"1991","unstructured":"Dershowitz, N., Jouannaud, J.: Notations for rewriting. Bull. EATCS 43, 162\u2013174 (1991)","journal-title":"Bull. EATCS"},{"key":"9590_CR28","unstructured":"Eder, E.: An implementation of a theorem prover based on the connection method. In: AIMSA\u201984, pp. 121\u2013128. North-Holland (1985)"},{"key":"9590_CR29","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: SAT\u00a0\u201905, LNCS, vol. 3569, pp. 61\u201375. Springer (2005)","DOI":"10.1007\/11499107_5"},{"issue":"1","key":"9590_CR30","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.tcs.2004.10.033","volume":"336","author":"R Fagin","year":"2005","unstructured":"Fagin, R., Kolaitis, P.G., Miller, R.J., Popa, L.: Data exchange: semantics and query answering. Theor. Comput. Sci. 336(1), 89\u2013124 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"9590_CR31","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, Berlin (1995)","edition":"2"},{"key":"9590_CR32","unstructured":"Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In: KR\u201992, pp. 425\u2013435. Morgan Kaufmann (1992)"},{"issue":"2","key":"9590_CR33","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)","journal-title":"ACM Trans. Database Syst."},{"key":"9590_CR34","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1613\/jair.3949","volume":"47","author":"BC Grau","year":"2013","unstructured":"Grau, B.C., Horrocks, I., Kr\u00f6tzsch, 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\u2013808 (2013)","journal-title":"JAIR"},{"key":"9590_CR35","doi-asserted-by":"crossref","unstructured":"Hoder, K., Holzer, A., Kov\u00e1cs, L., Voronkov, A.: Vinter: A Vampire-based tool for interpolation. In: APLAS 2012, LNCS, vol. 7705, pp. 148\u2013156. Springer (2012)","DOI":"10.1007\/978-3-642-35182-2_11"},{"key":"9590_CR36","doi-asserted-by":"crossref","unstructured":"Huang, G.: Constructing Craig interpolation formulas. In: COCOON \u201995, LNCS, vol. 959, pp. 181\u2013190. Springer (1995)","DOI":"10.1007\/BFb0030832"},{"key":"9590_CR37","doi-asserted-by":"crossref","unstructured":"Hudek, A., Toman, D., Wedell, G.: On enumerating query plans using analytic tableau. In: TABLEAUX 2015, LNCS (LNAI), vol. 9323, pp. 339\u2013354. Springer (2015)","DOI":"10.1007\/978-3-319-24312-2_23"},{"key":"9590_CR38","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/B978-044450813-3\/50005-9","volume-title":"Handbook of Automatic Reasoning, chap.\u00a03","author":"R H\u00e4hnle","year":"2001","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automatic Reasoning, chap.\u00a03, vol. 1, pp. 101\u2013178. Elsevier, Amsterdam (2001)"},{"issue":"1\u20133","key":"9590_CR39","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10817-006-9046-x","volume":"38","author":"S Jacobs","year":"2007","unstructured":"Jacobs, S., Waldmann, U.: Comparing instance generation methods for automated reasoning. J. Autom. Reason. 38(1\u20133), 57\u201378 (2007)","journal-title":"J. Autom. Reason."},{"key":"9590_CR40","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: TACAS 2010, LNCS, vol. 6015, pp. 129\u2013144 (2010)","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"9590_CR41","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C.: Efficient low-level connection tableaux. In: TABLEAUX 2015, LNCS (LNAI), vol. 9323, pp. 102\u2013111. Springer (2015)","DOI":"10.1007\/978-3-319-24312-2_8"},{"key":"9590_CR42","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J.: FEMaLeCoP: Fairly efficient machine learning connection prover. In: LPAR-20, LNCS, vol. 9450, pp. 88\u201396. Springer (2015)","DOI":"10.1007\/978-3-662-48899-7_7"},{"key":"9590_CR43","doi-asserted-by":"crossref","unstructured":"Kiesl, B., Suda, M.: A unifying principle for clause elimination in first-order logic. In: CADE 26, LNCS (LNAI), vol. 10395, pp. 274\u2013290. Springer (2017)","DOI":"10.1007\/978-3-319-63046-5_17"},{"key":"9590_CR44","unstructured":"Kiesl, B., Suda, M., Seidl, M., Tompits, H., Biere, A.: Blocked clauses in first-order logic. In: LPAR-21, EPiC, vol.\u00a046, pp. 31\u201348 (2017)"},{"key":"9590_CR45","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order interpolation and interpolating proof systems. In: LPAR-21, EPiC, vol.\u00a046, pp. 49\u201364. EasyChair (2017)"},{"issue":"3","key":"9590_CR46","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1145\/1149114.1149117","volume":"7","author":"N Leone","year":"2006","unstructured":"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\u2013562 (2006)","journal-title":"ACM Trans. Comput. Log."},{"key":"9590_CR47","first-page":"43","volume-title":"Automated Deduction - A Basis for Applications","author":"R Letz","year":"1998","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, Amsterdam (1998)"},{"key":"9590_CR48","doi-asserted-by":"crossref","unstructured":"Letz, R.: First-order tableau methods. In: M.\u00a0D\u2019Agostino, D. M. Gabbay, R. H\u00e4hnle, J. Posegga (eds.) Handb. of Tableau Methods, pp. 125\u2013196. Kluwer Academic Publishers (1999)","DOI":"10.1007\/978-94-017-1754-0_3"},{"key":"9590_CR49","unstructured":"Letz, R.: Tableau and connection calculi. structure, complexity, implementation. Habilitationsschrift, TU M\u00fcnchen (1999). http:\/\/www2.tcs.ifi.lmu.de\/~letz\/habil.ps. Accessed 7 June 2020"},{"issue":"3","key":"9590_CR50","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R Letz","year":"1994","unstructured":"Letz, R., Mayr, K., Goller, C.: Controlled integration of the cut rule into connection tableaux calculi. J. Autom. Reason. 13(3), 297\u2013337 (1994)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9590_CR51","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. Reason. 8(2), 183\u2013212 (1992)","journal-title":"J. Autom. Reason."},{"key":"9590_CR52","doi-asserted-by":"publisher","first-page":"2015","DOI":"10.1016\/B978-044450813-3\/50030-8","volume-title":"Handbook of Automatic Reasoning","author":"R Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automatic Reasoning, vol. 1, pp. 2015\u20132114. Elsevier, Amsterdam (2001)"},{"key":"9590_CR53","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":"9590_CR54","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)","journal-title":"Pac. J. Math."},{"issue":"4","key":"9590_CR55","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/320107.320115","volume":"4","author":"D Maier","year":"1979","unstructured":"Maier, D., Mendelzon, A.O., Sagiv, Y.: Testing implications of data dependencies. ACM Trans. Database Syst. 4(4), 455\u2013469 (1979)","journal-title":"ACM Trans. Database Syst."},{"key":"9590_CR56","doi-asserted-by":"crossref","unstructured":"Marx, M.: Queries determined by views: Pack your views. In: PODS\u00a0\u201907, pp. 23\u201330. ACM (2007)","DOI":"10.1145\/1265530.1265534"},{"key":"9590_CR57","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). http:\/\/www.cs.unm.edu\/~mccune\/prover9"},{"key":"9590_CR58","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: CAV 2003, LNCS, vol. 2725, pp. 1\u201313. Springer (2003)","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"9590_CR59","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Applications of Craig interpolants in model checking. In: TACAS 2005, LNCS, vol. 3440, pp. 1\u201312. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_1"},{"issue":"1","key":"9590_CR60","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101\u2013121 (2005)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"9590_CR61","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M Moser","year":"1997","unstructured":"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\u2013246 (1997)","journal-title":"J. Autom. Reason."},{"key":"9590_CR62","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1613\/jair.2811","volume":"36","author":"B Motik","year":"2009","unstructured":"Motik, B., Shearer, R., Horrocks, I.: Hypertableau reasoning for description logics. JAIR 36, 165\u2013228 (2009)","journal-title":"JAIR"},{"key":"9590_CR63","doi-asserted-by":"crossref","unstructured":"Motohashi, N.: Equality and Lyndon\u2019s interpolation theorem. J. Symb. Log. 49(1), 123\u2013128 (1984)","DOI":"10.2307\/2274095"},{"key":"9590_CR64","doi-asserted-by":"crossref","unstructured":"Nash, A., Segoufin, L., Vianu, V.: Views and queries: Determinacy and rewriting. ACM Trans. Database Systems 35(3) (2010)","DOI":"10.1145\/1806907.1806913"},{"key":"9590_CR65","unstructured":"Oliver, B.E., Otten, J.: Equality preprocessing in connection calculi. In: PAAR-2020, CEUR Workshop Proceedings (2020)"},{"issue":"2\u20133","key":"9590_CR66","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)","journal-title":"AI Commun."},{"key":"9590_CR67","unstructured":"Pelzer, B., Wernhard, C.: System description: E-KRHyper. In: CADE-21, LNCS (LNAI), vol. 4603, pp. 503\u2013513. Springer (2007)"},{"key":"9590_CR68","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)","journal-title":"J. Symb. Comput."},{"key":"9590_CR69","unstructured":"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"},{"key":"9590_CR70","doi-asserted-by":"crossref","unstructured":"Schulz, S., Cruanes, S., Vukmirovic, P.: Faster, higher, stronger: E 2.3. In: CADE\u00a027, LNCS, vol. 11716, pp. 495\u2013507. Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_29"},{"issue":"4","key":"9590_CR71","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."},{"key":"9590_CR72","doi-asserted-by":"crossref","unstructured":"Segoufin, L., Vianu, V.: Views and queries: determinacy and rewriting. In: PODS\u00a02005, pp. 49\u201360. ACM (2005)","DOI":"10.1145\/1065167.1065174"},{"key":"9590_CR73","doi-asserted-by":"crossref","unstructured":"Smullyan, R.M.: First-Order Logic. Springer (1968). Also republished with corrections by Dover publications (1995)","DOI":"10.1007\/978-3-642-86718-7"},{"issue":"4","key":"9590_CR74","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. Reason. 4(4), 353\u2013380 (1988)","journal-title":"J. Autom. Reason."},{"key":"9590_CR75","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/BF00172286","volume":"5","author":"A Tarski","year":"1935","unstructured":"Tarski, A.: Einige methologische Untersuchungen zur Definierbarkeit der Begriffe. Erkenntnis 5, 80\u2013100 (1935)","journal-title":"Erkenntnis"},{"key":"9590_CR76","doi-asserted-by":"publisher","DOI":"10.2200\/S00363ED1V01Y201105DTM018","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, New York (2011)"},{"key":"9590_CR77","unstructured":"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.\u00a01. EasyChair (2017)"},{"key":"9590_CR78","first-page":"115","volume-title":"Studies in Constructive Mathematics and Mathematical Logic","author":"GS Tseitin","year":"1970","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, London (1970)"},{"key":"9590_CR79","unstructured":"Wernhard, C.: System Description: KRHyper. Tech. Rep. Fachberichte Informatik 14\u20132003, Universit\u00e4t Koblenz-Landau, Koblenz, Germany (2003)"},{"key":"9590_CR80","doi-asserted-by":"crossref","unstructured":"Wernhard, C.: Semantic knowledge partitioning. In: JELIA 04, LNAI, vol. 3229, pp. 552\u2013564. Springer (2004)","DOI":"10.1007\/978-3-540-30227-8_46"},{"key":"9590_CR81","unstructured":"Wernhard, C.: The PIE system for proving, interpolating and eliminating. In: PAAR-2016, CEUR Workshop Proceedings, vol. 1635, pp. 125\u2013138 (2016)"},{"key":"9590_CR82","unstructured":"Wernhard, C.: Craig interpolation and access interpolation with clausal first-order tableaux. CoRR abs\/1802.04982 (2018). (Tech. rep. Technische Universit\u00e4t Dresden, KRR 18-01)"},{"key":"9590_CR83","doi-asserted-by":"crossref","unstructured":"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\u2013177 (2020)","DOI":"10.1007\/978-3-030-46714-2_11"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09590-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09590-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09590-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,2]],"date-time":"2021-06-02T06:07:48Z","timestamp":1622614068000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09590-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,27]]},"references-count":83,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2021,6]]}},"alternative-id":["9590"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09590-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2021,5,27]]},"assertion":[{"value":"18 October 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 March 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 May 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}