{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:36:24Z","timestamp":1759638984969,"version":"3.41.0"},"reference-count":30,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T00:00:00Z","timestamp":1497830400000},"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":[[2018,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper presents an example of formal reasoning about the semantics of a Prolog program of practical importance (the SAT solver of Howe and King). The program is treated as a definite clause logic program with added control. The logic program is constructed by means of stepwise refinement, hand in hand with its correctness and completeness proofs. The proofs are declarative \u2013 they do not refer to any operational semantics. Each step of the logic program construction follows a systematic approach to constructing programs which are provably correct and complete. We also prove that correctness and completeness of the logic program is preserved in the final Prolog program. Additionally, we prove termination, occur-check freedom and non-floundering.<\/jats:p><jats:p>Our example shows how dealing with \u201clogic\u201d and with \u201ccontrol\u201d can be separated. Most of the proofs can be done at the \u201clogic\u201d level, abstracting from any operational semantics.<\/jats:p><jats:p>The example employs approximate specifications; they are crucial in simplifying reasoning about logic programs. It also shows that the paradigm of semantics-preserving program transformations may be not sufficient. We suggest considering transformations which preserve correctness and completeness with respect to an approximate specification.<\/jats:p>","DOI":"10.1017\/s1471068417000047","type":"journal-article","created":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T02:31:01Z","timestamp":1497839461000},"page":"1-29","source":"Crossref","is-referenced-by-count":7,"title":["Logic + control: On program construction and verification"],"prefix":"10.1017","volume":"18","author":[{"given":"W\u0141ODZIMIERZ","family":"DRABENT","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2017,6,19]]},"reference":[{"doi-asserted-by":"publisher","key":"S1471068417000047_ref13","DOI":"10.1145\/2898434"},{"key":"S1471068417000047_ref9","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3345.001.0001","volume-title":"A Grammatical View of Logic Programming","author":"Deransart","year":"1993"},{"volume-title":"Logic Programming: Systematic Program Development","year":"1990","author":"Deville","key":"S1471068417000047_ref10"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref15","DOI":"10.1007\/s00165-016-0392-0"},{"key":"S1471068417000047_ref14","first-page":"498","article-title":"On definite program answers and least Herbrand models","volume":"16","author":"Drabent","year":"2016","journal-title":"TPLP"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref17","DOI":"10.1145\/1352582.1352585"},{"key":"S1471068417000047_ref16","first-page":"669","article-title":"Proving correctness and completeness of normal programs \u2013 a declarative approach","volume":"5","author":"Drabent","year":"2005","journal-title":"TPLP"},{"unstructured":"Drabent W. 2015. On completeness of logic programs. In Logic Based Program Synthesis and Transformation, LOPSTR 2014. Revised Selected Papers. Lecture Notes in Computer Science, vol. 8981. Springer. Extended version in CoRR abs\/1411.3015 (2014). http:\/\/arxiv.org\/abs\/1411.3015.","key":"S1471068417000047_ref12"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref4","DOI":"10.1016\/0743-1066(93)90014-8"},{"key":"S1471068417000047_ref5","first-page":"35","article-title":"SICStus Prolog \u2013 the first 25 years","volume":"12","author":"Carlsson","year":"2012","journal-title":"TPLP"},{"unstructured":"Apt K. R. 1997. From Logic Programming to Prolog. International Series in Computer Science. Prentice-Hall.","key":"S1471068417000047_ref1"},{"unstructured":"King A. 2012. Private communication.","key":"S1471068417000047_ref20"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref21","DOI":"10.1145\/359131.359136"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref2","DOI":"10.1007\/3-540-60043-4_47"},{"key":"S1471068417000047_ref29","first-page":"289","volume-title":"Proc. of Logic Programming Synthesis and Transformation, LOPSTR'98","author":"Smaus","year":"1998"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref22","DOI":"10.1016\/B978-0-934613-40-8.50020-8"},{"volume-title":"Types in Logic Programming","year":"1992","author":"Pfenning","key":"S1471068417000047_ref27"},{"key":"S1471068417000047_ref25","first-page":"369","article-title":"Classes of terminating logic programs","volume":"2","author":"Pedreschi","year":"2002","journal-title":"TPLP"},{"key":"S1471068417000047_ref11","first-page":"301","volume-title":"Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)","author":"Drabent","year":"2012"},{"key":"S1471068417000047_ref30","first-page":"73","volume-title":"Proc. of Principles of Declarative Programming, PLILP'98","author":"Smaus","year":"1998"},{"key":"S1471068417000047_ref28","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1192.001.0001","volume-title":"Algorithmic Program Debugging","author":"Shapiro","year":"1983"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref26","DOI":"10.1007\/978-3-642-14309-0_6"},{"key":"S1471068417000047_ref23","first-page":"33","article-title":"Polytool: Polynomial interpretations as a basis for termination analysis of logic programs","volume":"11","author":"Nguyen","year":"2011","journal-title":"TPLP"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref7","DOI":"10.1145\/368273.368557"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref19","DOI":"10.1016\/j.tcs.2012.02.024"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref18","DOI":"10.1016\/S1574-6526(07)03002-7"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref8","DOI":"10.1016\/0304-3975(93)90107-5"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref3","DOI":"10.1006\/inco.1993.1051"},{"doi-asserted-by":"publisher","key":"S1471068417000047_ref24","DOI":"10.1016\/S0743-1066(98)10035-3"},{"unstructured":"Clark K. L. 1979. Predicate Logic as Computational Formalism. Technical Report 79\/59, Imperial College, London. December.","key":"S1471068417000047_ref6"}],"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\/S1471068417000047","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T18:59:28Z","timestamp":1750359568000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068417000047\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,19]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["S1471068417000047"],"URL":"https:\/\/doi.org\/10.1017\/s1471068417000047","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2017,6,19]]}}}