liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Logic + Control: An Example
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology. Institute of Computer Science, Polish Academy of Sciences. (TCSLAB)
2012 (English)In: Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) / [ed] Agostino Dovier and Vítor Santos Costa, Dagstuhl Publishing , 2012, 301-311 p.Conference paper, Oral presentation only (Other academic)
Abstract [en]

We present a Prolog program (the SAT solver of Howe and King) as a 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 specication. This is augmented by a proof of termination under any selection rule. Correctness and termination 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 justication is presented.

For proving correctness we use a method, which should be well known but is often neglected. A contribution of this paper is a method for proving completeness. In particular we introduce a notion of semi-completeness, for which a local sucient condition exists.

We compare the proof methods with declarative diagnosis (algorithmic debugging). We introduce a method of proving that a certain kind of pruning preserves completeness. 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.

Place, publisher, year, edition, pages
Dagstuhl Publishing , 2012. 301-311 p.
Series
LIPICS, Leibnitz International Proceedings in Informatics, ISSN 1868-8969 ; Vol. 17
Keyword [en]
Logic programming, program correctness, program completeness, specication, declarative programming, declarative diagnosis
National Category
Computer Science
Identifiers
URN: urn:nbn:se:liu:diva-79508DOI: 10.4230/LIPIcs.ICLP.2012.301ISBN: 978-3-939897-43-9 (print)OAI: oai:DiVA.org:liu-79508DiVA: diva2:543156
Conference
28th International Conference on Logic Programming (ICLP-2012), 4-8 September, Budapest, Hungary
Available from: 2012-08-06 Created: 2012-08-06 Last updated: 2014-11-04Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Drabent, Wlodzimierz

Search in DiVA

By author/editor
Drabent, Wlodzimierz
By organisation
Software and SystemsThe Institute of Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 50 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf