{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,15]],"date-time":"2023-01-15T11:28:30Z","timestamp":1673782110127},"reference-count":41,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2007,11,1]],"date-time":"2007-11-01T00:00:00Z","timestamp":1193875200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2007,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In answer set programming (ASP), a problem at hand is solved by (i) writing a logic program whose answer sets correspond to the solutions of the problem, and by (ii) computing the answer sets of the program using an<jats:italic>answer set solver<\/jats:italic>as a search engine. Typically, a programmer creates a series of gradually improving logic programs for a particular problem when optimizing program length and execution time on a particular solver. This leads the programmer to a meta-level problem of ensuring that the programs are equivalent, i.e., they give rise to the same answer sets. To ease answer set programming at methodological level, we propose a translation-based method for verifying the equivalence of logic programs. The basic idea is to translate logic programs<jats:italic>P<\/jats:italic>and<jats:italic>Q<\/jats:italic>under consideration into a single logic program EQT(<jats:italic>P<\/jats:italic>,<jats:italic>Q<\/jats:italic>) whose answer sets (if such exist) yield counter-examples to the equivalence of<jats:italic>P<\/jats:italic>and<jats:italic>Q<\/jats:italic>. The method is developed here in a slightly more general setting by taking the<jats:italic>visibility<\/jats:italic>of atoms properly into account when comparing answer sets. The translation-based approach presented in the paper has been implemented as a translator called<jats:sc>lpeq<\/jats:sc>that enables the verification of weak equivalence within the<jats:sc>smodels<\/jats:sc>system using the same search engine as for the search of models. Our experiments with<jats:sc>lpeq<\/jats:sc>and<jats:sc>smodels<\/jats:sc>suggest that establishing the equivalence of logic programs in this way is in certain cases much faster than naive cross-checking of answer sets.<\/jats:p>","DOI":"10.1017\/s1471068407003031","type":"journal-article","created":{"date-parts":[[2007,5,25]],"date-time":"2007-05-25T09:58:55Z","timestamp":1180087135000},"page":"697-744","source":"Crossref","is-referenced-by-count":8,"title":["Automated Verification of Weak Equivalence within the<scp><i>smodels<\/i><\/scp>System"],"prefix":"10.1017","volume":"7","author":[{"given":"TOMI","family":"JANHUNEN","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"EMILIA","family":"OIKARINEN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2007,11,1]]},"reference":[{"key":"S1471068407003031_ref41","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068403001819"},{"key":"S1471068407003031_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30227-8_18"},{"key":"S1471068407003031_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-934613-40-8.50006-3"},{"key":"S1471068407003031_ref37","first-page":"195","volume-title":"Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming","author":"Soininen","year":"2001"},{"key":"S1471068407003031_ref15","first-page":"358","volume-title":"Proceedings of the 16th European Conference on Artificial Intelligence","author":"Janhunen","year":"2004"},{"key":"S1471068407003031_ref24","first-page":"170","volume-title":"Principles of Knowledge Representation and Reasoning: Proceedings of the 8th International Conference","author":"Lin","year":"2002"},{"key":"S1471068407003031_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-60085-2_17"},{"key":"S1471068407003031_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83189-8"},{"key":"S1471068407003031_ref7","first-page":"87","volume-title":"Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning","author":"Eiter","year":"2004"},{"key":"S1471068407003031_ref40","first-page":"434","volume-title":"Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning","author":"Syrj\u00e4nen","year":"2001"},{"key":"S1471068407003031_ref35","unstructured":"Simons P. 1999. Extending the stable model semantics with more expressive rules. In Proceedings of the 5th International Conference on Logic Programming and Nonmonotonic Reasoning. Springer-Verlag, pp. 305\u2013316. LNAI 1730."},{"key":"S1471068407003031_ref16","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.16.35-86"},{"key":"S1471068407003031_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(94)00092-1"},{"key":"S1471068407003031_ref38","unstructured":"Syrj\u00e4nen T. 2001. Lparse 1.0 user's manual. Available at http:\/\/www.tcs.hut.fi\/Software\/smodels."},{"key":"S1471068407003031_ref32","first-page":"412","volume-title":"Proceedings of the 17th European Conference on Artificial Intelligence","author":"Oikarinen","year":"2006"},{"key":"S1471068407003031_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10020-1"},{"key":"S1471068407003031_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/1149114.1149117"},{"key":"S1471068407003031_ref12","first-page":"579","volume-title":"Proceedings of the 7th International Conference on Logic Programming","author":"Gelfond","year":"1990"},{"key":"S1471068407003031_ref25","first-page":"112","volume-title":"Proceedings of the 18th National Conference on Artificial Intelligence","author":"Lin","year":"2002"},{"key":"S1471068407003031_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/116825.116836"},{"key":"S1471068407003031_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/11546207_39"},{"key":"S1471068407003031_ref30","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018930122475"},{"key":"S1471068407003031_ref3","first-page":"169","volume-title":"Proceedings of the Third International Symposium on Practical Aspects of Declarative Languages","author":"Balduccini","year":"2001"},{"key":"S1471068407003031_ref5","doi-asserted-by":"crossref","unstructured":"Dovier A. , Formisano A. and Pontelli E. 2005. A comparison of CLP(FD) and ASP solutions to NP-complete problems. In Proceedings of Convegno Italiano di Logica Computazionale. Italian Association for Logic Programming (GULP), Rome, Italy. Available at http:\/\/www.disp.uniroma2.it\/CILC2005\/.","DOI":"10.1007\/11562931_8"},{"key":"S1471068407003031_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/1119439.1119440"},{"key":"S1471068407003031_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(84)90014-1"},{"key":"S1471068407003031_ref8","unstructured":"Eiter T. , Tompits H. and Woltran S. 2005. On solution correspondences in answer-set programming. In Proceedings of the 19th International Joint Conference on Artificial Intelligence, IJCAI'05. Professional Book Center, Edinburgh, Scotland, UK, pp. 97\u2013102."},{"key":"S1471068407003031_ref9","first-page":"85","volume-title":"Proceedings of the 11th International Workshop on Nonmonotonic Reasoning","author":"Eiter","year":"2006"},{"key":"S1471068407003031_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00207-2"},{"key":"S1471068407003031_ref11","first-page":"1070","volume-title":"Proceedings of the 5th International Conference on Logic Programming","author":"Gelfond","year":"1988"},{"key":"S1471068407003031_ref17","first-page":"411","volume-title":"Principles of Knowledge Representation and Reasoning: Proceedings of the 7th International Conference","author":"Janhunen","year":"2000"},{"key":"S1471068407003031_ref22","first-page":"346","volume-title":"Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning","author":"Lierler","year":"2004"},{"key":"S1471068407003031_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/11546207_18"},{"key":"S1471068407003031_ref14","unstructured":"Janhunen T. 2003. Translatability and intranslatability results for certain classes of logic programs. Series A: Research report 82, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland. November. Available at http:\/\/www.tcs.hut.fi\/Publications\/series-a.shtml."},{"key":"S1471068407003031_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00187-X"},{"key":"S1471068407003031_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45757-7_41"},{"key":"S1471068407003031_ref20","first-page":"336","volume-title":"Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning","author":"Janhunen","year":"2004"},{"key":"S1471068407003031_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/383779.383783"},{"key":"S1471068407003031_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/11546207_37"},{"key":"S1471068407003031_ref31","first-page":"180","volume-title":"Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning","author":"Oikarinen","year":"2004"},{"key":"S1471068407003031_ref33","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/3-540-45329-6_31","volume-title":"Proceedings of the 10th Portuguese Conference on Artificial Intelligence","author":"Pearce","year":"2001"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068407003031","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T09:54:12Z","timestamp":1556445252000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068407003031\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,11]]},"references-count":41,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2007,11]]}},"alternative-id":["S1471068407003031"],"URL":"https:\/\/doi.org\/10.1017\/s1471068407003031","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,11]]}}}