{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:40Z","timestamp":1750220680623,"version":"3.41.0"},"reference-count":82,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2020,12,2]],"date-time":"2020-12-02T00:00:00Z","timestamp":1606867200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"FWF projects \u201cFormal Methods for Comparing and Optimizing Nonmonotonic Logic Programs\u201d","award":["P18019"],"award-info":[{"award-number":["P18019"]}]},{"name":"\u201cMethods and Methodologies for Developing Answer-set Programs\u201d","award":["P21698"],"award-info":[{"award-number":["P21698"]}]},{"name":"\u201cTreating Hard Problems with Decomposition and Dynamic Programming\u201d","award":["Y698"],"award-info":[{"award-number":["Y698"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2021,1,31]]},"abstract":"<jats:p>\n            This article deals with advanced notions of equivalence between nonmonotonic logic programs under the answer-set semantics, a topic of considerable interest, because such notions form the basis for program verification and are useful for program optimisation, debugging, and modular programming. In fact, there is extensive research in answer-set programming (ASP) dealing with different notions of equivalence between programs. Prominent among these notions is\n            <jats:italic>uniform equivalence<\/jats:italic>\n            , which checks whether two programs have the same semantics when joined with an arbitrary set of facts. In this article, we study a family of more fine-grained versions of uniform equivalence, viz.\n            <jats:italic>relativised uniform equivalence with projection<\/jats:italic>\n            , which extends standard uniform equivalence in terms of two additional parameters: one for specifying the input alphabet and one for specifying the output alphabet for programs. In particular, the second parameter is used for\n            <jats:italic>projecting<\/jats:italic>\n            answer sets to a set of designated output atoms. Answer-set projection, in particular, allows to compare programs that make use of different auxiliary atoms, which is important for practical programming aspects. We introduce novel semantic characterisations for the program correspondence problems under consideration and analyse their computational complexity. In the general case, deciding these problems lies on the third level of the polynomial hierarchy. Therefore, this task cannot be efficiently reduced to propositional answer-set programs itself (under the usual complexity-theoretic assumptions). However, reductions to\n            <jats:italic>quantified Boolean formulas<\/jats:italic>\n            (QBFs) are feasible. Indeed, we provide efficient (in fact, linear-time constructible) reductions to QBFs and discuss simplifications for certain special cases. These QBF reductions yield the basis for a prototype implementation, the system cc \u22a4, for deciding correspondence problems by using off-the-shelf QBF solvers. We discuss an application of cc \u22a4 for verifying the correctness of solutions by students drawn from a laboratory course on logic programming and knowledge representation at the Technische Universit\u00e4t Wien, employing relativised uniform equivalence with projection as the underlying program correspondence notion.\n          <\/jats:p>","DOI":"10.1145\/3422361","type":"journal-article","created":{"date-parts":[[2020,12,2]],"date-time":"2020-12-02T19:26:47Z","timestamp":1606937207000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Beyond Uniform Equivalence between Answer-set Programs"],"prefix":"10.1145","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9902-7662","authenticated-orcid":false,"given":"Johannes","family":"Oetsch","sequence":"first","affiliation":[{"name":"Bosch Center for Artificial Intelligence, Germany, and Technische Universit\u00e4t Wien, Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[{"name":"Johannes Kepler Universit\u00e4t Linz, Linz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans","family":"Tompits","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Wien, Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Woltran","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Wien, Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,12,2]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1017\/S147106841300001X"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 16th European Conference on Artificial Intelligence (ECAI\u201904)","volume":"110","author":"Arieli Ofer","year":"2004","unstructured":"Ofer Arieli . 2004 . Paraconsistent preferential reasoning by signed quantified Boolean formulae . In Proceedings of the 16th European Conference on Artificial Intelligence (ECAI\u201904) (Frontiers in Artificial Intelligence and Applications), Ramon L\u00f3pez de M\u00e1ntaras and Lorenza Saitta (Ed.) , Vol. 110 . IOS Press, Amsterdam, 773--777. Ofer Arieli. 2004. Paraconsistent preferential reasoning by signed quantified Boolean formulae. In Proceedings of the 16th European Conference on Artificial Intelligence (ECAI\u201904) (Frontiers in Artificial Intelligence and Applications), Ramon L\u00f3pez de M\u00e1ntaras and Lorenza Saitta (Ed.), Vol. 110. IOS Press, Amsterdam, 773--777."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 4th International Conference on Computational Models of Argument (COMMA\u201912)","volume":"245","author":"Arieli Ofer","unstructured":"Ofer Arieli and Martin W . \u00c3. Caminada. 2012. A general QBF-based formalization of abstract argumentation theory . In Proceedings of the 4th International Conference on Computational Models of Argument (COMMA\u201912) (Frontiers in Artificial Intelligence and Applications), Bart Verheij, Stefan Szeider, and Stefan Woltran (Eds.) , Vol. 245 . IOS Press, Amsterdam, 105--116. Ofer Arieli and Martin W. \u00c3. Caminada. 2012. A general QBF-based formalization of abstract argumentation theory. In Proceedings of the 4th International Conference on Computational Models of Argument (COMMA\u201912) (Frontiers in Artificial Intelligence and Applications), Bart Verheij, Stefan Szeider, and Stefan Woltran (Eds.), Vol. 245. IOS Press, Amsterdam, 105--116."},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1093\/logcom\/13.4.557"},{"volume-title":"Cambridge University Press","author":"Baral Chitta","unstructured":"Chitta Baral . 2003. Knowledge Representation , Reasoning, and Declarative Problem Solving . Cambridge University Press , Cambridge , England . Chitta Baral. 2003. Knowledge Representation, Reasoning, and Declarative Problem Solving. Cambridge University Press, Cambridge, England.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","volume-title":"Fredman","author":"Baral Chitta","year":"2000","unstructured":"Chitta Baral and Michael L . Fredman . 2000 . Reasoning agents in dynamic domains. In Logic-based Artificial Intelligence, Jack Minker (Ed.). Kluwer Academic Publishers , Dordrecht, 257--279. Chitta Baral and Michael L. Fredman. 2000. Reasoning agents in dynamic domains. In Logic-based Artificial Intelligence, Jack Minker (Ed.). Kluwer Academic Publishers, Dordrecht, 257--279."},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.5555\/1642293.1642301"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1007\/11532231_27"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1016\/j.artint.2009.06.006"},{"volume-title":"Inconsistency Tolerance (Lecture Notes in Computer Science), Leopoldo E","author":"Besnard Philippe","unstructured":"Philippe Besnard , Torsten Schaub , Hans Tompits , and Stefan Woltran . 2005. Representing paraconsistent reasoning via quantified propositional logic . In Inconsistency Tolerance (Lecture Notes in Computer Science), Leopoldo E . Bertossi, Anthony Hunter, and Torsten Schaub (Eds.), Vol. 3300 . Springer , Berlin , 84--118. Philippe Besnard, Torsten Schaub, Hans Tompits, and Stefan Woltran. 2005. Representing paraconsistent reasoning via quantified propositional logic. In Inconsistency Tolerance (Lecture Notes in Computer Science), Leopoldo E. Bertossi, Anthony Hunter, and Torsten Schaub (Eds.), Vol. 3300. Springer, Berlin, 84--118.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","first-page":"3","article-title":"Equivalence between answer-set programs under (partially) fixed input","volume":"83","author":"Bliem Bernhard","year":"2018","unstructured":"Bernhard Bliem and Stefan Woltran . 2018 . Equivalence between answer-set programs under (partially) fixed input . Ann. Math. Artific. Intell. 83 , 3 -- 4 (2018), 277--295. Bernhard Bliem and Stefan Woltran. 2018. Equivalence between answer-set programs under (partially) fixed input. Ann. Math. Artific. Intell. 83, 3--4 (2018), 277--295.","journal-title":"Ann. Math. Artific. Intell."},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1007\/11799573_21"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1007\/s10817-007-9082-1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1007\/11546207_43"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1093\/logcom\/14.6.801"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201908)","author":"Delgrande James P.","year":"2008","unstructured":"James P. Delgrande , Torsten Schaub , Hans Tompits , and Stefan Woltran . 2008 . Belief revision of logic programs under answer set semantics . In Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201908) , Gerhard Brewka and J\u00e9r\u00f4me Lang (Eds.). AAAI Press, Menlo Park, CA, 411--421. James P. Delgrande, Torsten Schaub, Hans Tompits, and Stefan Woltran. 2008. Belief revision of logic programs under answer set semantics. In Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201908), Gerhard Brewka and J\u00e9r\u00f4me Lang (Eds.). AAAI Press, Menlo Park, CA, 411--421."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 7th Conference on Artificial Intelligence (AAAI\u201900) and of the 12th Conference on Innovative Applications of Artificial Intelligence (IAAI\u201900)","author":"Egly Uwe","year":"2000","unstructured":"Uwe Egly , Thomas Eiter , Hans Tompits , and Stefan Woltran . 2000 . Solving advanced reasoning tasks using quantified Boolean formulas . In Proceedings of the 7th Conference on Artificial Intelligence (AAAI\u201900) and of the 12th Conference on Innovative Applications of Artificial Intelligence (IAAI\u201900) , Henry A. Kautz and Bruce W. Porter (Eds.). AAAI Press, Menlo Park, CA, 417--422. Uwe Egly, Thomas Eiter, Hans Tompits, and Stefan Woltran. 2000. Solving advanced reasoning tasks using quantified Boolean formulas. In Proceedings of the 7th Conference on Artificial Intelligence (AAAI\u201900) and of the 12th Conference on Innovative Applications of Artificial Intelligence (IAAI\u201900), Henry A. Kautz and Bruce W. Porter (Eds.). AAAI Press, Menlo Park, CA, 417--422."},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1007\/978-3-540-24605-3_17"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 17th European Conference on Artificial Intelligence (ECAI\u201906)","volume":"141","author":"Egly Uwe","year":"2006","unstructured":"Uwe Egly , Martina Seidl , and Stefan Woltran . 2006 . A solver for QBFs in nonprenex form . In Proceedings of the 17th European Conference on Artificial Intelligence (ECAI\u201906) (Frontiers in Artificial Intelligence and Applications), Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso (Eds.) , Vol. 141 . IOS Press, Amsterdam, 477--481. Uwe Egly, Martina Seidl, and Stefan Woltran. 2006. A solver for QBFs in nonprenex form. In Proceedings of the 17th European Conference on Artificial Intelligence (ECAI\u201906) (Frontiers in Artificial Intelligence and Applications), Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso (Eds.), Vol. 141. IOS Press, Amsterdam, 477--481."},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1007\/s10601-008-9055-y"},{"key":"e_1_2_1_21_1","first-page":"1","article-title":"The diagnosis frontend of the DLV system","volume":"12","author":"Eiter Thomas","year":"1999","unstructured":"Thomas Eiter , Wolfgang Faber , Nicola Leone , and Gerald Pfeifer . 1999 . The diagnosis frontend of the DLV system . AI Commun. 12 , 1 -- 2 (1999), 99--111. Thomas Eiter, Wolfgang Faber, Nicola Leone, and Gerald Pfeifer. 1999. The diagnosis frontend of the DLV system. AI Commun. 12, 1--2 (1999), 99--111.","journal-title":"AI Commun."},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1007\/3-540-44957-4_54"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1007\/11546207_42"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1007\/978-3-540-24599-5_16"},{"key":"e_1_2_1_25_1","first-page":"1","article-title":"Model-based recasting in answer-set programming","volume":"23","author":"Eiter Thomas","year":"2013","unstructured":"Thomas Eiter , Michael Fink , J\u00f6rg P\u00fchrer , Hans Tompits , and Stefan Woltran . 2013 . Model-based recasting in answer-set programming . J. Appl. Non-Class. Logics 23 , 1 -- 2 (2013), 75--104. Thomas Eiter, Michael Fink, J\u00f6rg P\u00fchrer, Hans Tompits, and Stefan Woltran. 2013. Model-based recasting in answer-set programming. J. Appl. Non-Class. Logics 23, 1--2 (2013), 75--104.","journal-title":"J. Appl. Non-Class. Logics"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR\u201904)","volume":"2923","author":"Eiter Thomas","year":"2004","unstructured":"Thomas Eiter , Michael Fink , Hans Tompits , and Stefan Woltran . 2004 . Simplifying logic programs under uniform and strong equivalence . In Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR\u201904) (Lecture Notes in Computer Science), Vladimir Lifschitz and Ilkka Niemel\u00e4 (Eds.) , Vol. 2923 . Springer, Berlin, 87--99. Thomas Eiter, Michael Fink, Hans Tompits, and Stefan Woltran. 2004. Simplifying logic programs under uniform and strong equivalence. In Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR\u201904) (Lecture Notes in Computer Science), Vladimir Lifschitz and Ilkka Niemel\u00e4 (Eds.), Vol. 2923. Springer, Berlin, 87--99."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 20th National Conference on Artificial Intelligence (AAAI\u201905)","author":"Eiter Thomas","year":"2005","unstructured":"Thomas Eiter , Michael Fink , Hans Tompits , and Stefan Woltran . 2005 . Strong and uniform equivalence in answer-set programming: Characterizations and complexity results for the non-ground case . In Proceedings of the 20th National Conference on Artificial Intelligence (AAAI\u201905) , Manuela M. Veloso and Subbarao Kambhampati (Eds.). AAAI Press, Menlo Park, CA, 695--700. Thomas Eiter, Michael Fink, Hans Tompits, and Stefan Woltran. 2005. Strong and uniform equivalence in answer-set programming: Characterizations and complexity results for the non-ground case. In Proceedings of the 20th National Conference on Artificial Intelligence (AAAI\u201905), Manuela M. Veloso and Subbarao Kambhampati (Eds.). AAAI Press, Menlo Park, CA, 695--700."},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1145\/1243996.1244000"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1007\/BF01536399"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.5555\/1642293.1642309"},{"doi-asserted-by":"publisher","key":"e_1_2_1_31_1","DOI":"10.1017\/S1471068406002729"},{"doi-asserted-by":"publisher","key":"e_1_2_1_32_1","DOI":"10.1017\/S1471068410000542"},{"volume-title":"Answer Set Solving in Practice. Morgan 8 Claypool Publishers","author":"Gebser Martin","unstructured":"Martin Gebser , Roland Kaminski , Benjamin Kaufmann , and Torsten Schaub . 2012. Answer Set Solving in Practice. Morgan 8 Claypool Publishers , San Rafael, CA . Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. 2012. Answer Set Solving in Practice. Morgan 8 Claypool Publishers, San Rafael, CA.","key":"e_1_2_1_33_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.5555\/1625275.1625336"},{"doi-asserted-by":"publisher","key":"e_1_2_1_35_1","DOI":"10.1007\/978-3-030-19570-0_36"},{"volume-title":"The Answer-Set Programming Approach","author":"Gelfond Michael","unstructured":"Michael Gelfond and Yulia Kahl . 2014. Knowledge Representation , Reasoning, and the Design of Intelligent Agents : The Answer-Set Programming Approach . Cambridge University Press , Cambridge, England . Michael Gelfond and Yulia Kahl. 2014. Knowledge Representation, Reasoning, and the Design of Intelligent Agents: The Answer-Set Programming Approach. Cambridge University Press, Cambridge, England.","key":"e_1_2_1_36_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1007\/BF03037169"},{"unstructured":"Enrico Giunchiglia Massimo Narizzano Luca Pulina and Armando Tacchella. 2005. Quantified Boolean Formulas Satisfiability Library (QBFLIB). Retrieved from www.qbflib.org.  Enrico Giunchiglia Massimo Narizzano Luca Pulina and Armando Tacchella. 2005. Quantified Boolean Formulas Satisfiability Library (QBFLIB). Retrieved from www.qbflib.org.","key":"e_1_2_1_38_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.1609\/aaai.v33i01.33012843"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI\u201916)","volume":"285","author":"Gon\u00e7alves Ricardo","year":"2016","unstructured":"Ricardo Gon\u00e7alves , Matthias Knorr , and Jo\u00e3o Leite . 2016 . You can\u2019t always forget what you want: On the limits of forgetting in answer set programming . In Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI\u201916) (Frontiers in Artificial Intelligence and Applications), Gal A. Kaminka, Maria Fox, Paolo Bouquet, Eyke H\u00fcllermeier, Virginia Dignum, Frank Dignum, and Frank van Harmelen (Eds.) , Vol. 285 . IOS Press, Amsterdam, 957--965. Ricardo Gon\u00e7alves, Matthias Knorr, and Jo\u00e3o Leite. 2016. You can\u2019t always forget what you want: On the limits of forgetting in answer set programming. In Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI\u201916) (Frontiers in Artificial Intelligence and Applications), Gal A. Kaminka, Maria Fox, Paolo Bouquet, Eyke H\u00fcllermeier, Virginia Dignum, Frank Dignum, and Frank van Harmelen (Eds.), Vol. 285. IOS Press, Amsterdam, 957--965."},{"doi-asserted-by":"publisher","key":"e_1_2_1_41_1","DOI":"10.1007\/11799573_22"},{"doi-asserted-by":"publisher","key":"e_1_2_1_42_1","DOI":"10.1007\/978-3-540-30227-8_17"},{"volume-title":"Correct Reasoning\u2014Essays on Logic-Based AI in Honour of Vladimir Lifschitz (Lecture Notes in Computer Science)","author":"Janhunen Tomi","unstructured":"Tomi Janhunen and Ilkka Niemel\u00e4 . 2012. Applying visible strong equivalence in answer-set program transformations . In Correct Reasoning\u2014Essays on Logic-Based AI in Honour of Vladimir Lifschitz (Lecture Notes in Computer Science) , Esra Erdem, Joohyung Lee, Yuliya Lierler, and David Pearce (Eds.), Vol. 7265 . Springer , Berlin , 363--379. Tomi Janhunen and Ilkka Niemel\u00e4. 2012. Applying visible strong equivalence in answer-set program transformations. In Correct Reasoning\u2014Essays on Logic-Based AI in Honour of Vladimir Lifschitz (Lecture Notes in Computer Science), Esra Erdem, Joohyung Lee, Yuliya Lierler, and David Pearce (Eds.), Vol. 7265. Springer, Berlin, 363--379.","key":"e_1_2_1_43_1"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the 19th European Conference on Artificial Intelligence (ECAI\u201910)","volume":"215","author":"Janhunen Tomi","year":"2010","unstructured":"Tomi Janhunen , Ilkka Niemel\u00e4 , Johannes Oetsch , J\u00f6rg P\u00fchrer , and Hans Tompits . 2010 . On testing answer-set programs . In Proceedings of the 19th European Conference on Artificial Intelligence (ECAI\u201910) (Frontiers in Artificial Intelligence and Applications), Helder Coelho, Rudi Studer, and Michael J. Wooldridge (Eds.) , Vol. 215 . IOS Press, Amsterdam, 951--956. Tomi Janhunen, Ilkka Niemel\u00e4, Johannes Oetsch, J\u00f6rg P\u00fchrer, and Hans Tompits. 2010. On testing answer-set programs. In Proceedings of the 19th European Conference on Artificial Intelligence (ECAI\u201910) (Frontiers in Artificial Intelligence and Applications), Helder Coelho, Rudi Studer, and Michael J. Wooldridge (Eds.), Vol. 215. IOS Press, Amsterdam, 951--956."},{"doi-asserted-by":"publisher","key":"e_1_2_1_45_1","DOI":"10.1007\/978-3-642-20895-9_26"},{"doi-asserted-by":"publisher","key":"e_1_2_1_46_1","DOI":"10.1145\/1119439.1119440"},{"doi-asserted-by":"publisher","key":"e_1_2_1_47_1","DOI":"10.1017\/S1471068407003031"},{"doi-asserted-by":"publisher","key":"e_1_2_1_48_1","DOI":"10.1145\/1149114.1149117"},{"doi-asserted-by":"publisher","key":"e_1_2_1_49_1","DOI":"10.1145\/383779.383783"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the 11th International Conference on Logic Programming (ICLP\u201994)","author":"Lifschitz Vladimir","year":"1994","unstructured":"Vladimir Lifschitz and Hudson Turner . 1994 . Splitting a logic program . In Proceedings of the 11th International Conference on Logic Programming (ICLP\u201994) , Pascal Van Hentenryck (Ed.). MIT Press, Cambridge, MA, 23--37. Vladimir Lifschitz and Hudson Turner. 1994. Splitting a logic program. In Proceedings of the 11th International Conference on Logic Programming (ICLP\u201994), Pascal Van Hentenryck (Ed.). MIT Press, Cambridge, MA, 23--37."},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 8th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201902)","author":"Lin Fangzhen","year":"2002","unstructured":"Fangzhen Lin . 2002 . Reducing strong equivalence of logic programs to entailment in classical propositional logic . In Proceedings of the 8th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201902) , Dieter Fensel, Fausto Giunchiglia, Deborah L. McGuinness, and Mary-Anne Williams (Eds.). Morgan Kaufmann Publishers, Inc., San Francisco, CA, 170--176. Fangzhen Lin. 2002. Reducing strong equivalence of logic programs to entailment in classical propositional logic. In Proceedings of the 8th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201902), Dieter Fensel, Fausto Giunchiglia, Deborah L. McGuinness, and Mary-Anne Williams (Eds.). Morgan Kaufmann Publishers, Inc., San Francisco, CA, 170--176."},{"doi-asserted-by":"publisher","key":"e_1_2_1_52_1","DOI":"10.5555\/1622591.1622603"},{"doi-asserted-by":"publisher","key":"e_1_2_1_53_1","DOI":"10.1007\/978-3-642-20895-9_15"},{"volume-title":"Proceedings of the 5th Annual ACM Symposium on Theory of Computing (STOC\u201973)","author":"Albert","unstructured":"Albert R. Meyer and Larry J. Stockmeyer. 1973. Word problems requiring exponential time: Preliminary report . In Proceedings of the 5th Annual ACM Symposium on Theory of Computing (STOC\u201973) , Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, and H. Raymond Strong (Eds.). ACM Press, New York, 1--9. Albert R. Meyer and Larry J. Stockmeyer. 1973. Word problems requiring exponential time: Preliminary report. In Proceedings of the 5th Annual ACM Symposium on Theory of Computing (STOC\u201973), Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, and H. Raymond Strong (Eds.). ACM Press, New York, 1--9.","key":"e_1_2_1_54_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_55_1","DOI":"10.5555\/1662603.1662607"},{"doi-asserted-by":"publisher","key":"e_1_2_1_56_1","DOI":"10.1007\/978-3-642-31612-8_33"},{"doi-asserted-by":"publisher","key":"e_1_2_1_57_1","DOI":"10.1007\/3-540-45241-9_12"},{"doi-asserted-by":"publisher","key":"e_1_2_1_58_1","DOI":"10.1109\/CIC.2006.29"},{"doi-asserted-by":"publisher","key":"e_1_2_1_59_1","DOI":"10.1007\/978-3-642-04238-6_32"},{"doi-asserted-by":"publisher","key":"e_1_2_1_60_1","DOI":"10.1007\/978-3-540-89982-2_49"},{"key":"e_1_2_1_61_1","volume-title":"Proceedings of the 22nd National Conference on Artificial Intelligence (AAAI\u201907)","author":"Oetsch Johannes","year":"2007","unstructured":"Johannes Oetsch , Hans Tompits , and Stefan Woltran . 2007 . Facts do not cease to exist because they are ignored: Relativised uniform equivalence with answer-set projection . In Proceedings of the 22nd National Conference on Artificial Intelligence (AAAI\u201907) , Robert C. Holte and Adele Howe (Eds.). AAAI Press, Menlo Park, CA, 458--464. Johannes Oetsch, Hans Tompits, and Stefan Woltran. 2007. Facts do not cease to exist because they are ignored: Relativised uniform equivalence with answer-set projection. In Proceedings of the 22nd National Conference on Artificial Intelligence (AAAI\u201907), Robert C. Holte and Adele Howe (Eds.). AAAI Press, Menlo Park, CA, 458--464."},{"key":"e_1_2_1_62_1","volume-title":"Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR\u201904)","volume":"2923","author":"Oikarinen Emilia","year":"2004","unstructured":"Emilia Oikarinen and Tomi Janhunen . 2004 . Verifying the equivalence of logic programs in the disjunctive case . In Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR\u201904) (Lecture Notes in Computer Science), Vladimir Lifschitz and Ilkka Niemel\u00e4 (Eds.) , Vol. 2923 . Springer, Berlin, 180--193. Emilia Oikarinen and Tomi Janhunen. 2004. Verifying the equivalence of logic programs in the disjunctive case. In Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR\u201904) (Lecture Notes in Computer Science), Vladimir Lifschitz and Ilkka Niemel\u00e4 (Eds.), Vol. 2923. Springer, Berlin, 180--193."},{"key":"e_1_2_1_63_1","volume-title":"Proceedings of the 17th European Conference on Artificial Intelligence (ECAI\u201906)","volume":"141","author":"Oikarinen Emilia","year":"2006","unstructured":"Emilia Oikarinen and Tomi Janhunen . 2006 . Modular equivalence for normal logic programs . In Proceedings of the 17th European Conference on Artificial Intelligence (ECAI\u201906) (Frontiers in Artificial Intelligence and Applications), Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso (Eds.) , Vol. 141 . IOS Press, Amsterdam, 412--416. Emilia Oikarinen and Tomi Janhunen. 2006. Modular equivalence for normal logic programs. In Proceedings of the 17th European Conference on Artificial Intelligence (ECAI\u201906) (Frontiers in Artificial Intelligence and Applications), Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso (Eds.), Vol. 141. IOS Press, Amsterdam, 412--416."},{"volume-title":"Computational Complexity","author":"Papadimitriou Christos H.","unstructured":"Christos H. Papadimitriou . 1994. Computational Complexity . Addison-Wesley Publishing , Reading, MA . Christos H. Papadimitriou. 1994. Computational Complexity. Addison-Wesley Publishing, Reading, MA.","key":"e_1_2_1_64_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_65_1","DOI":"10.1007\/978-3-540-27775-0_15"},{"doi-asserted-by":"publisher","key":"e_1_2_1_66_1","DOI":"10.1017\/S147106840999010X"},{"key":"e_1_2_1_67_1","volume-title":"Answer Set Programming and Constraints (Dagstuhl Seminar Proceedings), Gerhard Brewka, Ilkka Niemel\u00e4, Torsten Schaub, and Miros\u0142aw Truszczy\u0144ski (Eds.)","volume":"05171","author":"Polleres Axel","year":"2005","unstructured":"Axel Polleres . 2005 . Semantic web languages and semantic web services as application areas for answer set programming. In Nonmonotonic Reasoning , Answer Set Programming and Constraints (Dagstuhl Seminar Proceedings), Gerhard Brewka, Ilkka Niemel\u00e4, Torsten Schaub, and Miros\u0142aw Truszczy\u0144ski (Eds.) , Vol. 05171 . Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, Germany, Dagstuhl, Germany, Article 5, 6 pages. Retrieved from http:\/\/drops.dagstuhl.de\/opus\/volltexte\/ 2005\/263. Axel Polleres. 2005. Semantic web languages and semantic web services as application areas for answer set programming. In Nonmonotonic Reasoning, Answer Set Programming and Constraints (Dagstuhl Seminar Proceedings), Gerhard Brewka, Ilkka Niemel\u00e4, Torsten Schaub, and Miros\u0142aw Truszczy\u0144ski (Eds.), Vol. 05171. Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, Germany, Dagstuhl, Germany, Article 5, 6 pages. Retrieved from http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2005\/263."},{"doi-asserted-by":"publisher","key":"e_1_2_1_68_1","DOI":"10.1007\/978-3-540-89982-2_47"},{"doi-asserted-by":"publisher","key":"e_1_2_1_69_1","DOI":"10.1016\/0004-3702(87)90062-2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_70_1","DOI":"10.5555\/1622859.1622870"},{"key":"e_1_2_1_71_1","volume-title":"Proceedings of the 22nd AAAI Conference on Artificial Intelligence (AAAI\u201907)","author":"Rintanen Jussi","year":"2007","unstructured":"Jussi Rintanen . 2007 . Asymptotically optimal encodings of conformant planning in QBF . In Proceedings of the 22nd AAAI Conference on Artificial Intelligence (AAAI\u201907) , Robert C. Holte and Adele Howe (Eds.). AAAI Press, Menlo Park, CA, 1015--1050. Jussi Rintanen. 2007. Asymptotically optimal encodings of conformant planning in QBF. In Proceedings of the 22nd AAAI Conference on Artificial Intelligence (AAAI\u201907), Robert C. Holte and Adele Howe (Eds.). AAAI Press, Menlo Park, CA, 1015--1050."},{"volume-title":"Foundations of Deductive Databases and Logic Programming, Jack Minker (Ed.). Morgan Kaufmann","author":"Sagiv Yehoshua","unstructured":"Yehoshua Sagiv . 1988. Optimizing Datalog programs . In Foundations of Deductive Databases and Logic Programming, Jack Minker (Ed.). Morgan Kaufmann , San Francisco, CA , 659--698. Yehoshua Sagiv. 1988. Optimizing Datalog programs. In Foundations of Deductive Databases and Logic Programming, Jack Minker (Ed.). Morgan Kaufmann, San Francisco, CA, 659--698.","key":"e_1_2_1_72_1"},{"key":"e_1_2_1_73_1","volume-title":"Steklov Mathematical Institute, Leningrad","volume":"8","author":"Ed Anatol Olesjewitsch","year":"1970","unstructured":"Anatol Olesjewitsch Slisenko ( Ed .). 1970 . Studies in Constructive Mathematics and Mathematical Logic, Part II. Seminars in Mathematics, V. A . Steklov Mathematical Institute, Leningrad , Vol. 8 . Consultants Bureau, New York. Anatol Olesjewitsch Slisenko (Ed.). 1970. Studies in Constructive Mathematics and Mathematical Logic, Part II. Seminars in Mathematics, V. A. Steklov Mathematical Institute, Leningrad, Vol. 8. Consultants Bureau, New York."},{"key":"e_1_2_1_74_1","volume-title":"Proceedings of the 1st International Workshop on Practical Aspects of Declarative Languages (PADL \u201999)","volume":"1551","author":"Soininen Timo","year":"1999","unstructured":"Timo Soininen and Ilkka Niemel\u00e4 . 1999 . Developing a declarative rule language for applications in product configuration . In Proceedings of the 1st International Workshop on Practical Aspects of Declarative Languages (PADL \u201999) (Lecture Notes in Computer Science), Gopal Gupta (Ed.) , Vol. 1551 . Springer, Berlin, 305--319. Timo Soininen and Ilkka Niemel\u00e4. 1999. Developing a declarative rule language for applications in product configuration. In Proceedings of the 1st International Workshop on Practical Aspects of Declarative Languages (PADL \u201999) (Lecture Notes in Computer Science), Gopal Gupta (Ed.), Vol. 1551. Springer, Berlin, 305--319."},{"doi-asserted-by":"publisher","key":"e_1_2_1_75_1","DOI":"10.1016\/0304-3975(76)90061-X"},{"doi-asserted-by":"publisher","key":"e_1_2_1_76_1","DOI":"10.1007\/11562931_16"},{"key":"e_1_2_1_77_1","volume-title":"Proceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201906)","author":"Truszczy\u0144ski Miros\u0142aw","year":"2006","unstructured":"Miros\u0142aw Truszczy\u0144ski . 2006 . Strong and uniform equivalence of nonmonotonic theories\u2014An algebraic approach . In Proceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201906) , Patrick Doherty, John Mylopoulos, and Christopher A. Welty (Eds.). AAAI Press, Menlo Park, CA, 389--399. Miros\u0142aw Truszczy\u0144ski. 2006. Strong and uniform equivalence of nonmonotonic theories\u2014An algebraic approach. In Proceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning (KR\u201906), Patrick Doherty, John Mylopoulos, and Christopher A. Welty (Eds.). AAAI Press, Menlo Park, CA, 389--399."},{"doi-asserted-by":"publisher","key":"e_1_2_1_78_1","DOI":"10.5555\/1735390.1735393"},{"key":"e_1_2_1_79_1","first-page":"234","article-title":"O Slozhnosti Vyvoda v Ischislenii Vyskazyvanij","volume":"8","author":"Tseitin Grigori S.","year":"1968","unstructured":"Grigori S. Tseitin . 1968 . O Slozhnosti Vyvoda v Ischislenii Vyskazyvanij . Zapiski Nauchnykh Seminarov LOMI 8 (1968), 234 -- 259 . English translation: [73, pp. 115--125]. Grigori S. Tseitin. 1968. O Slozhnosti Vyvoda v Ischislenii Vyskazyvanij. Zapiski Nauchnykh Seminarov LOMI 8 (1968), 234--259. English translation: [73, pp. 115--125].","journal-title":"Zapiski Nauchnykh Seminarov LOMI"},{"doi-asserted-by":"publisher","key":"e_1_2_1_80_1","DOI":"10.1017\/S1471068403001819"},{"doi-asserted-by":"publisher","key":"e_1_2_1_81_1","DOI":"10.1007\/978-3-540-30227-8_16"},{"doi-asserted-by":"publisher","key":"e_1_2_1_82_1","DOI":"10.1017\/S1471068407003250"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3422361","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3422361","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:03:21Z","timestamp":1750197801000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3422361"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12,2]]},"references-count":82,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1,31]]}},"alternative-id":["10.1145\/3422361"],"URL":"https:\/\/doi.org\/10.1145\/3422361","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2020,12,2]]},"assertion":[{"value":"2019-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-12-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}