Logic + control: An example

Author Wlodzimierz Drabent

Thumbnail PDF


  • Filesize: 478 kB
  • 11 pages

Document Identifiers

Author Details

Wlodzimierz Drabent

Cite AsGet BibTex

Wlodzimierz Drabent. Logic + control: An example. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 17, pp. 301-311, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


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.
  • program correctness
  • program completeness
  • specification
  • declarative programming
  • declarative diagnosis.


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads