{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:40:06Z","timestamp":1747593606771,"version":"3.40.5"},"publisher-location":"Cham","reference-count":78,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031634970"},{"type":"electronic","value":"9783031634987"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We show a projective Beth definability theorem for logic programs under the stable model semantics: For given programs <jats:italic>P<\/jats:italic> and <jats:italic>Q<\/jats:italic> and vocabulary\u00a0<jats:italic>V<\/jats:italic> (set of predicates) the existence of a program\u00a0<jats:italic>R<\/jats:italic> in <jats:italic>V<\/jats:italic> such that <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$P \\cup R$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>P<\/mml:mi>\n                    <mml:mo>\u222a<\/mml:mo>\n                    <mml:mi>R<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> and <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$P \\cup Q$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>P<\/mml:mi>\n                    <mml:mo>\u222a<\/mml:mo>\n                    <mml:mi>Q<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> are strongly equivalent can be expressed as a first-order entailment. Moreover, our result is effective: A program\u00a0<jats:italic>R<\/jats:italic> can be constructed from a Craig interpolant for this entailment, using a known first-order encoding for testing strong equivalence, which we apply in reverse to extract programs from formulas. As a further perspective, this allows transforming logic programs via transforming their first-order encodings. In a prototypical implementation, the Craig interpolation is performed by first-order provers based on clausal tableaux or resolution calculi. Our work shows how definability and interpolation, which underlie modern logic-based approaches to advanced tasks in knowledge representation, transfer to answer set programming.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_11","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"172-193","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Synthesizing Strongly Equivalent Logic Programs: Beth Definability for\u00a0Answer Set Programs via\u00a0Craig Interpolation in\u00a0First-Order Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-1545-9356","authenticated-orcid":false,"given":"Jan","family":"Heuer","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0438-8829","authenticated-orcid":false,"given":"Christoph","family":"Wernhard","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/3-540-45757-7_20","volume-title":"Logics in Artificial Intelligence","author":"E Amir","year":"2002","unstructured":"Amir, E.: Interpolation theorems for nonmonotonic reasoning systems. In: Flesca, S., Greco, S., Ianni, G., Leone, N. (eds.) JELIA 2002. LNCS (LNAI), vol. 2424, pp. 233\u2013244. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45757-7_20"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Artale, A., Jung, J.C., Mazzullo, A., Ozaki, A., Wolter, F.: Living without Beth and Craig: definitions and interpolants in description and modal logics with nominals and role inclusions. ACM Trans. Comp. Log. 24(4), 34:1\u201334:51 (2023). https:\/\/doi.org\/10.1145\/3597301","DOI":"10.1145\/3597301"},{"key":"11_CR3","volume-title":"Knowledge Representation, Reasoning and Declarative Problem Solving","author":"C Baral","year":"2010","unstructured":"Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, Cambridge (2010)"},{"key":"11_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":"11_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-01856-5","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 (2016). https:\/\/doi.org\/10.1007\/978-3-031-01856-5","journal-title":"Morgan & Claypool"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Benedikt, M., Pradic, C., Wernhard, C.: Synthesizing nested relational queries from implicit specifications. In: PODS 2023, pp. 33\u201345. ACM (2023). https:\/\/doi.org\/10.1145\/3584372.3588653","DOI":"10.1145\/3584372.3588653"},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1016\/S1385-7258(53)50042-3","volume":"15","author":"EW Beth","year":"1953","unstructured":"Beth, E.W.: On Padoa\u2019s method in the theory of definition. Indag. Math. 15, 330\u2013339 (1953)","journal-title":"Indag. Math."},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Bibel, W.: Automated Theorem Proving. Vieweg, Braunschweig (1987). https:\/\/doi.org\/10.1007\/978-3-322-90102-6. First edition 1982","DOI":"10.1007\/978-3-322-90102-6"},{"key":"11_CR9","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":"11_CR10","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. Reasoning 54(1), 69\u201397 (2015). https:\/\/doi.org\/10.1007\/s10817-014-9314-0","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"11_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0743-1066(98)10030-4","volume":"40","author":"S Brass","year":"1999","unstructured":"Brass, S., Dix, J.: Semantics of (disjunctive) logic programs based on partial evaluation. J. Log. Prog. 40(1), 1\u201346 (1999). https:\/\/doi.org\/10.1016\/S0743-1066(98)10030-4","journal-title":"J. Log. Prog."},{"issue":"6","key":"11_CR12","doi-asserted-by":"publisher","first-page":"745","DOI":"10.1017\/S1471068407003110","volume":"7","author":"P Cabalar","year":"2007","unstructured":"Cabalar, P., Ferraris, P.: Propositional theories are strongly equivalent to logic programs. Theory Pract. Log. Program. 7(6), 745\u2013759 (2007). https:\/\/doi.org\/10.1017\/S1471068407003110","journal-title":"Theory Pract. Log. Program."},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Cabalar, P., Kaminski, R., Morkisch, P., Schaub, T.: telingo = ASP + time. In: Balduccini, M., Lierler, Y., Woltran, S. (eds.) LPNMR 2019. LNCS, vol. 11481, pp. 256\u2013269. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20528-7_19","DOI":"10.1007\/978-3-030-20528-7_19"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-04238-6_8","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"P Cabalar","year":"2009","unstructured":"Cabalar, P., Pearce, D., Valverde, A.: A revised concept of safety for general answer set programs. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS (LNAI), vol. 5753, pp. 58\u201370. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04238-6_8"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/978-3-030-19570-0_44","volume-title":"Logics in Artificial Intelligence","author":"V Cassano","year":"2019","unstructured":"Cassano, V., Fervari, R., Areces, C., Castro, P.F.: Interpolation and Beth definability in default logics. In: Calimeri, F., Leone, N., Manna, M. (eds.) JELIA 2019. LNCS (LNAI), vol. 11468, pp. 675\u2013691. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-19570-0_44"},{"key":"11_CR16","unstructured":"ten Cate, B., Conradie, W., Marx, M., Venema, Y.: Definitorially complete description logics. In: Doherty, P., Mylopoulos, J., Welty, C.A. (eds.) KR\u00a02006, pp. 79\u201389. AAAI Press (2006). http:\/\/www.aaai.org\/Library\/KR\/2006\/kr06-011.php"},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1613\/JAIR.4057","volume":"48","author":"B ten Cate","year":"2013","unstructured":"ten Cate, B., Franconi, E., Seylan, I.: Beth definability in expressive description logics. JAIR 48, 347\u2013414 (2013). https:\/\/doi.org\/10.1613\/JAIR.4057","journal-title":"JAIR"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/11546207_43","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"Y Chen","year":"2005","unstructured":"Chen, Y., Lin, F., Li, L.: SELP \u2013 a system for studying strong equivalence between logic programs. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 442\u2013446. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11546207_43"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-1-4684-3384-5_11","volume-title":"Logic and Data Bases","author":"KL Clark","year":"1978","unstructured":"Clark, K.L.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, vol. 1, pp. 293\u2013322. Plenum Press, New York (1978)"},{"key":"11_CR20","doi-asserted-by":"publisher","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","DOI":"10.2307\/2963593"},{"issue":"3","key":"11_CR21","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."},{"key":"11_CR22","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1613\/JAIR.5530","volume":"60","author":"JP Delgrande","year":"2017","unstructured":"Delgrande, J.P.: A knowledge level account of forgetting. JAIR 60, 1165\u20131213 (2017). https:\/\/doi.org\/10.1613\/JAIR.5530","journal-title":"JAIR"},{"key":"11_CR23","unstructured":"Eiter, T., Tompits, H., Woltran, S.: On solution correspondences in answer-set programming. In: Kaelbling, L.P., Saffiotti, A. (eds.) IJCAI 2005, pp. 97\u2013102. Professional Book Center (2005). http:\/\/ijcai.org\/Proceedings\/05\/Papers\/1177.pdf"},{"issue":"4","key":"11_CR24","doi-asserted-by":"publisher","first-page":"933","DOI":"10.1017\/S1471068423000200","volume":"23","author":"J Fandinno","year":"2023","unstructured":"Fandinno, J., Hansen, Z., Lierler, Y., Lifschitz, V., Temple, N.: External behavior of a logic program and verification of refactoring. Theory Pract. Log. Program. 23(4), 933\u2013947 (2023). https:\/\/doi.org\/10.1017\/S1471068423000200","journal-title":"Theory Pract. Log. Program."},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Fandinno, J., Lifschitz, V.: On Heuer\u2019s procedure for verifying strong equivalence. In: Gaggl, S.A., Martinez, M.V., Ortiz, M. (eds.) JELIA 2023. LNCS, vol. 14281, pp. 253\u2013261. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43619-2_18","DOI":"10.1007\/978-3-031-43619-2_18"},{"issue":"5","key":"11_CR26","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1017\/S1471068420000344","volume":"20","author":"J Fandinno","year":"2020","unstructured":"Fandinno, J., Lifschitz, V., L\u00fchne, P., Schaub, T.: Verifying tight logic programs with anthem and Vampire. Theory Pract. Log. Program. 20(5), 735\u2013750 (2020). https:\/\/doi.org\/10.1017\/S1471068420000344","journal-title":"Theory Pract. Log. Program."},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Fandinno, J., Lifschitz, V., Temple, N.: Locally tight programs. Theory Pract. Log. Program., 1\u201331 (2024). https:\/\/doi.org\/10.1017\/S147106842300039X","DOI":"10.1017\/S147106842300039X"},{"issue":"1","key":"11_CR28","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1016\/J.ARTINT.2010.04.011","volume":"175","author":"P Ferraris","year":"2011","unstructured":"Ferraris, P., Lee, J., Lifschitz, V.: Stable models and circumscription. Artif. Intell. 175(1), 236\u2013263 (2011). https:\/\/doi.org\/10.1016\/J.ARTINT.2010.04.011","journal-title":"Artif. Intell."},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, New York (1995). https:\/\/doi.org\/10.1007\/978-1-4612-2360-3","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"11_CR30","volume-title":"Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications","author":"DM Gabbay","year":"2008","unstructured":"Gabbay, D.M., Schmidt, R.A., Sza\u0142as, A.: Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Publications, London (2008)"},{"key":"11_CR31","unstructured":"Gabbay, D.M., Pearce, D., Valverde, A.: Interpolable formulas in equilibrium logic and answer set programming. JAIR 42, 917\u2013943 (2011). https:\/\/jair.org\/index.php\/jair\/article\/view\/10743"},{"issue":"4\u20135","key":"11_CR32","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1017\/S1471068415000150","volume":"15","author":"M Gebser","year":"2015","unstructured":"Gebser, M., Harrison, A., Kaminski, R., Lifschitz, V., Schaub, T.: Abstract gringo. Theory Pract. Log Program 15(4\u20135), 449\u2013463 (2015). https:\/\/doi.org\/10.1017\/S1471068415000150","journal-title":"Theory Pract. Log Program"},{"key":"11_CR33","doi-asserted-by":"publisher","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., Wanko, P.: Theory solving made easy with Clingo 5. In: Carro, M., King, A., Saeedloei, N., Vos, M.D. (eds.) ICLP 2016. OASIcs, vol.\u00a052, pp. 2:1\u20132:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/OASICS.ICLP.2016.2","DOI":"10.4230\/OASICS.ICLP.2016.2"},{"issue":"1","key":"11_CR34","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1017\/S1471068418000054","volume":"19","author":"M Gebser","year":"2019","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Multi-shot ASP solving with Clingo. Theory Pract. Log. Program. 19(1), 27\u201382 (2019). https:\/\/doi.org\/10.1017\/S1471068418000054","journal-title":"Theory Pract. Log. Program."},{"key":"11_CR35","volume-title":"Handbook of Knowledge Representation, Foundations of Artificial Intelligence","author":"M Gelfond","year":"2008","unstructured":"Gelfond, M.: Answer sets. In: van Harmelen, F., Lifschitz, V., Porter, B.W. (eds.) Handbook of Knowledge Representation, Foundations of Artificial Intelligence, vol. 3. Elsevier, Amsterdam (2008)"},{"key":"11_CR36","first-page":"1070","volume-title":"ICLP\/SLP 1988","author":"M Gelfond","year":"1988","unstructured":"Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R.A., Bowen, K.A. (eds.) ICLP\/SLP 1988, pp. 1070\u20131080. MIT Press, Cambridge (1988)"},{"issue":"1","key":"11_CR37","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1017\/S1471068421000570","volume":"23","author":"R Gon\u00e7alves","year":"2023","unstructured":"Gon\u00e7alves, R., Knorr, M., Leite, J.: Forgetting in answer set programming - a survey. Theory Pract. Log. Program. 23(1), 111\u2013156 (2023). https:\/\/doi.org\/10.1017\/S1471068421000570","journal-title":"Theory Pract. Log. Program."},{"key":"11_CR38","unstructured":"Heuer, J.: Automated verification of equivalence properties in advanced logic programs. Bachelor\u2019s thesis, University of Potsdam (2020). https:\/\/arxiv.org\/abs\/2310.19806"},{"key":"11_CR39","unstructured":"Heuer, J.: Automated verification of equivalence properties in advanced logic programs. In: Schwarz, S., Wenzel, M. (eds.) WLP\u00a02023 (2023). https:\/\/dbs.informatik.uni-halle.de\/wlp2023\/ WLP2023_Heuer_Automated%20Verification%20of%20Equivalence%20Properties%20in%20Advanced%20Logic%20Programs.pdf"},{"key":"11_CR40","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"},{"issue":"5\u20136","key":"11_CR41","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1017\/S1471068417000242","volume":"17","author":"T Janhunen","year":"2017","unstructured":"Janhunen, T., Kaminski, R., Ostrowski, M., Schellhorn, S., Wanko, P., Schaub, T.: Clingo goes linear constraints over reals and integers. Theory Pract. Log. Program. 17(5\u20136), 872\u2013888 (2017). https:\/\/doi.org\/10.1017\/S1471068417000242","journal-title":"Theory Pract. Log. Program."},{"key":"11_CR42","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-540-24609-1_30","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"T Janhunen","year":"2003","unstructured":"Janhunen, T., Oikarinen, E.: LPEQ and DLPEQ \u2014 translators for automated equivalence testing of logic programs. In: Lifschitz, V., Niemel\u00e4, I. (eds.) LPNMR 2004. LNCS (LNAI), vol. 2923, pp. 336\u2013340. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-24609-1_30"},{"key":"11_CR43","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":"11_CR44","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":"11_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-540-89982-2_55","volume-title":"Logic Programming","author":"J Lee","year":"2008","unstructured":"Lee, J., Lifschitz, V., Palla, R.: Safe formulas in the general theory of stable models (preliminary report). In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 672\u2013676. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89982-2_55"},{"key":"11_CR46","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 5 Feb 2024"},{"issue":"2","key":"11_CR47","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":"11_CR48","unstructured":"Lifschitz, V.: Foundations of logic programming. In: Brewka, G. (ed.) Principles of Knowledge Representation, pp. 69\u2013128. CSLI Publications (1996). http:\/\/www.cs.utexas.edu\/users\/ai-lab?lif96b"},{"key":"11_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-642-15025-8_24","volume-title":"Fields of Logic and Computation","author":"V Lifschitz","year":"2010","unstructured":"Lifschitz, V.: Thirteen definitions of a stable model. In: Blass, A., Dershowitz, N., Reisig, W. (eds.) Fields of Logic and Computation. LNCS, vol. 6300, pp. 488\u2013503. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15025-8_24"},{"key":"11_CR50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24658-7","volume-title":"Answer Set Programming","author":"V Lifschitz","year":"2019","unstructured":"Lifschitz, V.: Answer Set Programming. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24658-7"},{"issue":"4","key":"11_CR51","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1017\/S1471068422000278","volume":"22","author":"V Lifschitz","year":"2022","unstructured":"Lifschitz, V.: Strong equivalence of logic programs with counting. Theory Pract. Log. Program. 22(4), 573\u2013588 (2022). https:\/\/doi.org\/10.1017\/S1471068422000278","journal-title":"Theory Pract. Log. Program."},{"key":"11_CR52","unstructured":"Lifschitz, V., L\u00fchne, P., Schaub, T.: Anthem: transforming gringo programs into first-order theories (preliminary report). CoRR (2018). http:\/\/arxiv.org\/abs\/1810.00453"},{"key":"11_CR53","doi-asserted-by":"publisher","unstructured":"Lifschitz, V., L\u00fchne, P., Schaub, T.: Verifying strong equivalence of programs in the input language of gringo. In: Balduccini, M., Lierler, Y., Woltran, S. (eds.) LPNMR 2019. LNCS, vol. 11481, pp. 270\u2013283. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20528-7_20","DOI":"10.1007\/978-3-030-20528-7_20"},{"issue":"4","key":"11_CR54","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1145\/383779.383783","volume":"2","author":"V Lifschitz","year":"2001","unstructured":"Lifschitz, V., Pearce, D., Valverde, A.: Strongly equivalent logic programs. ACM Trans. Comp. Log. 2(4), 526\u2013541 (2001). https:\/\/doi.org\/10.1145\/383779.383783","journal-title":"ACM Trans. Comp. Log."},{"key":"11_CR55","unstructured":"Lin, F.: Reducing strong equivalence of logic programs to entailment in classical propositional logic. In: KR 2002, pp. 170\u2013176. Morgan Kaufmann (2002)"},{"key":"11_CR56","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."},{"key":"11_CR57","doi-asserted-by":"publisher","unstructured":"Marek, V.W., Truszczynski, M.: Stable models and an alternative logic programming paradigm. In: Apt, K.R., Marek, V.W., Truszczynski, M., Warren, D.S. (eds.) The Logic Programming Paradigm - A 25-Year Perspective, pp. 375\u2013398. Artificial Intelligence. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-3-642-60085-2_17","DOI":"10.1007\/978-3-642-60085-2_17"},{"key":"11_CR58","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). http:\/\/www.cs.unm.edu\/~mccune\/prover9. Accessed 5 Feb 2024"},{"issue":"3","key":"11_CR59","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."},{"issue":"3\u20134","key":"11_CR60","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1023\/A:1018930122475","volume":"25","author":"I Niemel\u00e4","year":"1999","unstructured":"Niemel\u00e4, I.: Logic programs with stable model semantics as a constraint programming paradigm. Ann. Math. Artif. Intell. 25(3\u20134), 241\u2013273 (1999)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"2\u20133","key":"11_CR61","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":"05","key":"11_CR62","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1017\/S147106840999010X","volume":"9","author":"D Pearce","year":"2009","unstructured":"Pearce, D., Tompits, H., Woltran, S.: Characterising equilibrium logic and nested logic programs: Reductions and complexity. Theory Pract. Log. Program. 9(05), 565\u2013616 (2009). https:\/\/doi.org\/10.1017\/S147106840999010X","journal-title":"Theory Pract. Log. Program."},{"key":"11_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/978-3-540-89982-2_46","volume-title":"Logic Programming","author":"D Pearce","year":"2008","unstructured":"Pearce, D., Valverde, A.: Quantified equilibrium logic and foundations for answer set programs. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 546\u2013560. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89982-2_46"},{"issue":"1","key":"11_CR64","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1016\/J.JCSS.2011.02.013","volume":"78","author":"D Pearce","year":"2012","unstructured":"Pearce, D., Valverde, A.: Synonymous theories and knowledge representations in answer set programming. J. Comput. Syst. Sci. 78(1), 86\u2013104 (2012). https:\/\/doi.org\/10.1016\/J.JCSS.2011.02.013","journal-title":"J. Comput. Syst. Sci."},{"key":"11_CR65","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"},{"key":"11_CR66","doi-asserted-by":"crossref","unstructured":"Segoufin, L., Vianu, V.: Views and queries: determinacy and rewriting. In: PODS 2005, pp. 49\u201360. ACM (2005)","DOI":"10.1145\/1065167.1065174"},{"issue":"3","key":"11_CR67","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1145\/321592.321604","volume":"17","author":"JR Slagle","year":"1970","unstructured":"Slagle, J.R.: Interpolation theorems for resolution in lower predicate calculus. JACM 17(3), 535\u2013542 (1970). https:\/\/doi.org\/10.1145\/321592.321604","journal-title":"JACM"},{"key":"11_CR68","doi-asserted-by":"crossref","unstructured":"Smullyan, R.M.: First-Order Logic. Springer, Heidelberg (1968). Also republished with corrections by Dover publications, 1995","DOI":"10.1007\/978-3-642-86718-7"},{"issue":"4","key":"11_CR69","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":"11_CR70","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reasoning 59(4), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","DOI":"10.1007\/s10817-017-9407-7"},{"key":"11_CR71","unstructured":"Takeuti, G.: Proof Theory, 2nd edn. North-Holland, Amsterdam (1987)"},{"key":"11_CR72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-01881-7","author":"D Toman","year":"2011","unstructured":"Toman, D., Weddell, G.: Fundamentals of Physical Design and Query Compilation. Morgan & Claypool (2011). https:\/\/doi.org\/10.1007\/978-3-031-01881-7","journal-title":"Morgan & Claypool"},{"key":"11_CR73","doi-asserted-by":"publisher","unstructured":"Toman, D., Weddell, G.E.: First order rewritability in ontology-mediated querying in horn description logics. In: AAAI\u00a02022, IAAI\u00a02022, EAAI\u00a02022, pp. 5897\u20135905. AAAI Press (2022). https:\/\/doi.org\/10.1609\/AAAI.V36I5.20534","DOI":"10.1609\/AAAI.V36I5.20534"},{"key":"11_CR74","unstructured":"Wernhard, C.: The PIE system for proving, interpolating and eliminating. In: Fontaine, P., Schulz, S., Urban, J. (eds.) PAAR\u00a02016. CEUR Workshop Proceedings, vol.\u00a01635, pp. 125\u2013138. CEUR-WS.org (2016). http:\/\/ceur-ws.org\/Vol-1635\/paper-11.pdf"},{"key":"11_CR75","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":"11_CR76","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":"11_CR77","doi-asserted-by":"publisher","unstructured":"Wernhard, C.: Range-restricted and Horn interpolation through clausal tableaux. In: Ramanayake, R., Urban, J. (eds.) TABLEAUX 2023. LNCS (LNAI), vol. 14278, pp. 3\u201323. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43513-3_1","DOI":"10.1007\/978-3-031-43513-3_1"},{"issue":"1\u20132","key":"11_CR78","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1017\/S1471068411000494","volume":"12","author":"J Wielemaker","year":"2012","unstructured":"Wielemaker, J., Schrijvers, T., Triska, M., Lager, T.: SWI-Prolog. Theory Pract. Log Program 12(1\u20132), 67\u201396 (2012). https:\/\/doi.org\/10.1017\/S1471068411000494","journal-title":"Theory Pract. Log Program"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:16Z","timestamp":1747592236000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":78,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}