Correct Reasoning about Logic Programs

Kriener, Jael

doi:10.4230/LIPIcs.ICLP.2011.280

Document

Correct Reasoning about Logic Programs

Author Jael Kriener

Part of: Volume: Technical Communications of the 27th International Conference on Logic Programming (ICLP'11) (ICLP 2011)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: International Conference on Logic Programming (ICLP)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2011-06-27

PDF

File

PDF

LIPIcs.ICLP.2011.280.pdf

Filesize: 212 kB
4 pages

Document Identifiers

DOI: 10.4230/LIPIcs.ICLP.2011.280
URN: urn:nbn:de:0030-drops-31875

Subject Classification

Keywords

Prolog
cut
determinacy inference
abstract interpretation
denotational semantics
automated theorem proving
Coq

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

In this PhD project, we present an approach to the problem of determinacy inference in logic programs with cut, which treats cut uniformly and contextually. The overall aim is to develop a theoretical analysis, abstract it to a suitable domain and prove both the concrete analysis and the abstraction correct in a formal theorem prover (Coq). A crucial advantage of this approach, besides the guarantee of correctness, is the possibility of automatically extracting an implementation of the analysis.

Cite As Get BibTex

Jael Kriener. Correct Reasoning about Logic Programs. In Technical Communications of the 27th International Conference on Logic Programming (ICLP'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 11, pp. 280-283, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011) https://doi.org/10.4230/LIPIcs.ICLP.2011.280

Author Details

Jael Kriener

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail