{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T22:01:20Z","timestamp":1747173680307,"version":"3.40.5"},"reference-count":14,"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>This paper describes a generalization of Clark\u2019s completion that is applicable to logic programs containing arithmetic operations and produces syntactically simple, natural looking formulas. If a set of first-order axioms is equivalent to the completion of a program, then we may be able to find standard models of these axioms by running an answer set solver. As an example, we apply this \u201creverse completion\u201d procedure to the Sum and Product Puzzle.<\/jats:p>","DOI":"10.1017\/s1471068423000224","type":"journal-article","created":{"date-parts":[[2023,7,18]],"date-time":"2023-07-18T13:22:39Z","timestamp":1689686559000},"page":"664-677","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["On Program Completion, with an Application to the Sum and Product Puzzle"],"prefix":"10.1017","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6051-7907","authenticated-orcid":false,"given":"VLADIMIR","family":"LIFSCHITZ","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"S1471068423000224_ref6","unstructured":"Gebser, M. , Kaminski, R. , Kaufmann, B. , Lindauer, M. , Ostrowski, M. , Romero, J. , Schaub, T. and Thiele, S. 2019. Potassco User Guide. URL: https:\/\/github.com\/potassco\/guide\/releases\/."},{"key":"S1471068423000224_ref4","doi-asserted-by":"crossref","unstructured":"Fandinno, J. , Lifschitz, V. , L\u00fchne, P. and Schaub, T. 2020. Verifying tight logic programs with Anthem and Vampire. Theory and Practice of Logic Programming, 20.","DOI":"10.1017\/S1471068420000344"},{"key":"S1471068423000224_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20528-7_20"},{"key":"S1471068423000224_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068415000150"},{"key":"S1471068423000224_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(84)90011-6"},{"key":"S1471068423000224_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-75775-5_28"},{"key":"S1471068423000224_ref7","doi-asserted-by":"crossref","unstructured":"Lierler, Y. and Maratea, M. 2004. Cmodels-2: SAT-based answer set solver enhanced to non-tight programs. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), 346\u2013350.","DOI":"10.1007\/978-3-540-24609-1_32"},{"key":"S1471068423000224_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068419000450"},{"key":"S1471068423000224_ref2","doi-asserted-by":"crossref","unstructured":"Clark, K. 1978. Negation as failure. In Logic and Data Bases, H. Gallaire and J. Minker, Eds. Plenum Press, New York, 293\u2013322.","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"S1471068423000224_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.04.004"},{"key":"S1471068423000224_ref12","unstructured":"McCarthy, J. 1990. Formalization of two puzzles involving knowledge. In Formalizing Common Sense: Papers by John McCarthy. Ablex, Norwood, NJ."},{"key":"S1471068423000224_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037172"},{"volume-title":"Effective Theories in Programming Practice","year":"2022","author":"Misra","key":"S1471068423000224_ref13"},{"key":"S1471068423000224_ref14","doi-asserted-by":"crossref","unstructured":"van Ditmarsch, H. , Ruan, J. and Verbrugge, L. C. 2005. Model checking sum and product. In Proceedings of Australasian Joint Conference on Artificial Intelligence, 790\u2013795.","DOI":"10.1007\/11589990_82"}],"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\/S1471068423000224","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,27]],"date-time":"2024-02-27T09:38:20Z","timestamp":1709026700000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068423000224\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7]]},"references-count":14,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,7]]}},"alternative-id":["S1471068423000224"],"URL":"https:\/\/doi.org\/10.1017\/s1471068423000224","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"}]}}