{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T11:07:39Z","timestamp":1758280059436,"version":"3.40.5"},"reference-count":15,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2023,7,18]],"date-time":"2023-07-18T00:00:00Z","timestamp":1689638400000},"content-version":"unspecified","delay-in-days":17,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2023,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Refactoring is modifying a program without changing its external behavior. In this paper, we make the concept of external behavior precise for a simple answer set programming language. Then we describe a proof assistant for the task of verifying that refactoring a program in that language is performed correctly.<\/jats:p>","DOI":"10.1017\/s1471068423000200","type":"journal-article","created":{"date-parts":[[2023,7,18]],"date-time":"2023-07-18T13:44:52Z","timestamp":1689687892000},"page":"933-947","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":9,"title":["External Behavior of a Logic Program and Verification of Refactoring"],"prefix":"10.1017","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3917-8717","authenticated-orcid":false,"given":"JORGE","family":"FANDINNO","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8447-4048","authenticated-orcid":false,"given":"ZACHARY","family":"HANSEN","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6146-623X","authenticated-orcid":false,"given":"YULIYA","family":"LIERLER","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6051-7907","authenticated-orcid":false,"given":"VLADIMIR","family":"LIFSCHITZ","sequence":"additional","affiliation":[]},{"given":"NATHAN","family":"TEMPLE","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"S1471068423000200_ref3","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v36i5.20504"},{"key":"S1471068423000200_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89982-2_49"},{"key":"S1471068423000200_ref11","doi-asserted-by":"crossref","unstructured":"Kova\u0107s, L. and Voronkov, A. 2013. First-order theorem proving and Vampire. In International Conference on Computer Aided Verification, 1\u201335.","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"S1471068423000200_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139342124"},{"key":"S1471068423000200_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068415000150"},{"key":"S1471068423000200_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24599-5_46"},{"key":"S1471068423000200_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3158144"},{"key":"S1471068423000200_ref4","unstructured":"Fandinno, J. and Lifschitz, V. 2021. Verification of locally tight programs (extended abstract). In Technical Communications of the 37th International Conference on Logic Programming (ICLP)."},{"key":"S1471068423000200_ref8","doi-asserted-by":"crossref","unstructured":"Gebser, M. , Kaminski, R. , Kaufmann, B. and Schaub, T. 2011. Challenges in answer set solving. In Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning. Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday. Springer, 74\u201390.","DOI":"10.1007\/978-3-642-20832-4_6"},{"key":"S1471068423000200_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23264-5_17"},{"key":"S1471068423000200_ref9","doi-asserted-by":"crossref","unstructured":"Gelfond, M. 2002. Representing Knowledge in A-Prolog. Lecture Notes in Computer Science vol. 2408, 413\u2013451.","DOI":"10.1007\/3-540-45632-5_16"},{"key":"S1471068423000200_ref2","doi-asserted-by":"crossref","unstructured":"Clark, K. 1978. Negation as failure. In Logic and Data Bases, H. Gallaire and J. Minker, Eds. Press, Plenum , York, New , 293\u2013322.","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"S1471068423000200_ref7","unstructured":"Gebser, M. , Kaminski, R. , Kaufmann, B. , Lindauer, M. , Ostrowski, M. , Romero, J. , Schaub, T. and Thiele, S. 2019. Potassco User Guide. Available at https:\/\/github.com\/potassco\/guide\/releases\/."},{"key":"S1471068423000200_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068422000278"},{"key":"S1471068423000200_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068420000344"}],"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\/S1471068423000200","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,27]],"date-time":"2024-02-27T09:38:34Z","timestamp":1709026714000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068423000200\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7]]},"references-count":15,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,7]]}},"alternative-id":["S1471068423000200"],"URL":"https:\/\/doi.org\/10.1017\/s1471068423000200","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2023,7]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}