2026-07-20T05:47:09Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3631 2024-03-06T10:34:27Z ddc:004 open_access

Logic + control: An example Drabent, Wlodzimierz program correctness program completeness specification declarative programming declarative diagnosis. We present a Prolog program - the SAT solver of Howe and King - as a (pure) logic program with added control. The control consists of a selection rule (delays of Prolog) and pruning the search space. We construct the logic program together with proofs of its correctness and completeness, with respect to a formal specification. Correctness and termination of the logic program are inherited by the Prolog program; the change of selection rule preserves completeness. We prove that completeness is also preserved by one case of pruning; for the other an informal justification is presented. For proving correctness we use a method, which should be well known but is often neglected. For proving program completeness we employ a new, simpler variant of a method published previously. We point out usefulness of approximate specifications. We argue that the proof methods correspond to natural declarative thinking about programs, and that they can be used, formally or informally, in every-day programming. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Wlodzimierz Drabent 2012 Is Part Of LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICLP.2012.301 urn:nbn:de:0030-drops-36317 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2012.301 eng https://creativecommons.org/licenses/by-nd/3.0/legalcode