DROPS

Document

DOI: 10.4230/LIPIcs.ICLP.2012.301

Logic + control: An example

Authors: Wlodzimierz Drabent

Published in: LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012)

Abstract

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{drabent:LIPIcs.ICLP.2012.301,
  author =	{Drabent, Wlodzimierz},
  title =	{{Logic + control: An example}},
  booktitle =	{Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)},
  pages =	{301--311},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-43-9},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{17},
  editor =	{Dovier, Agostino and Santos Costa, V{\'\i}tor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2012.301},
  URN =		{urn:nbn:de:0030-drops-36317},
  doi =		{10.4230/LIPIcs.ICLP.2012.301},
  annote =	{Keywords: program correctness, program completeness, specification, declarative programming, declarative diagnosis.}
}

Search Results

Documents authored by Drabent, Wlodzimierz

Logic + control: An example

Abstract

Cite as

Thanks for your feedback!

Could not send message