Coalgebraic Derivations in Logic Programming

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

Coalgebra may be used to provide semantics for SLD-derivations, both finite and infinite. We first give such semantics to classical SLD-derivations, proving results such as adequacy, soundness and completeness. Then, based upon coalgebraic semantics, we propose a new sound and complete algorithm for parallel derivations. We analyse this new algorithm in terms of the Theory of Observables, and we prove soundness, completeness, correctness and full abstraction results.
Original languageEnglish
Title of host publicationComputer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
PublisherSchloss Dagstuhl - Leibniz-Zentrum fur Informatik
Pages352-366
Number of pages15
ISBN (Print)9783939897323
DOIs
Publication statusPublished - 2011

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik
Volume12
ISSN (Print)1868-8969

Fingerprint

Logic Programming
Soundness
Completeness
Coalgebra
Correctness
Semantics

Keywords

  • Logic programming
  • SLD-resolution
  • concurrency
  • coinduction
  • Lawvere theoriesm
  • coinductive logic programming
  • concurrent logic programming

Cite this

Komendantskaya, E., & Power, J. (2011). Coalgebraic Derivations in Logic Programming. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (pp. 352-366). (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 12). Schloss Dagstuhl - Leibniz-Zentrum fur Informatik. https://doi.org/10.4230/LIPIcs.CSL.2011.352
Komendantskaya, Ekaterina ; Power, John. / Coalgebraic Derivations in Logic Programming. Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Schloss Dagstuhl - Leibniz-Zentrum fur Informatik, 2011. pp. 352-366 (Leibniz International Proceedings in Informatics (LIPIcs)).
@inbook{ffc230ad9c71418aa92fb2122f72d4b6,
title = "Coalgebraic Derivations in Logic Programming",
abstract = "Coalgebra may be used to provide semantics for SLD-derivations, both finite and infinite. We first give such semantics to classical SLD-derivations, proving results such as adequacy, soundness and completeness. Then, based upon coalgebraic semantics, we propose a new sound and complete algorithm for parallel derivations. We analyse this new algorithm in terms of the Theory of Observables, and we prove soundness, completeness, correctness and full abstraction results.",
keywords = "Logic programming, SLD-resolution, concurrency, coinduction, Lawvere theoriesm, coinductive logic programming, concurrent logic programming",
author = "Ekaterina Komendantskaya and John Power",
year = "2011",
doi = "10.4230/LIPIcs.CSL.2011.352",
language = "English",
isbn = "9783939897323",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum fur Informatik",
pages = "352--366",
booktitle = "Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL",

}

Komendantskaya, E & Power, J 2011, Coalgebraic Derivations in Logic Programming. in Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), vol. 12, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik, pp. 352-366. https://doi.org/10.4230/LIPIcs.CSL.2011.352

Coalgebraic Derivations in Logic Programming. / Komendantskaya, Ekaterina; Power, John.

Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Schloss Dagstuhl - Leibniz-Zentrum fur Informatik, 2011. p. 352-366 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 12).

Research output: Chapter in Book/Report/Conference proceedingChapter

TY - CHAP

T1 - Coalgebraic Derivations in Logic Programming

AU - Komendantskaya, Ekaterina

AU - Power, John

PY - 2011

Y1 - 2011

N2 - Coalgebra may be used to provide semantics for SLD-derivations, both finite and infinite. We first give such semantics to classical SLD-derivations, proving results such as adequacy, soundness and completeness. Then, based upon coalgebraic semantics, we propose a new sound and complete algorithm for parallel derivations. We analyse this new algorithm in terms of the Theory of Observables, and we prove soundness, completeness, correctness and full abstraction results.

AB - Coalgebra may be used to provide semantics for SLD-derivations, both finite and infinite. We first give such semantics to classical SLD-derivations, proving results such as adequacy, soundness and completeness. Then, based upon coalgebraic semantics, we propose a new sound and complete algorithm for parallel derivations. We analyse this new algorithm in terms of the Theory of Observables, and we prove soundness, completeness, correctness and full abstraction results.

KW - Logic programming

KW - SLD-resolution

KW - concurrency

KW - coinduction

KW - Lawvere theoriesm

KW - coinductive logic programming

KW - concurrent logic programming

U2 - 10.4230/LIPIcs.CSL.2011.352

DO - 10.4230/LIPIcs.CSL.2011.352

M3 - Chapter

SN - 9783939897323

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 352

EP - 366

BT - Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL

PB - Schloss Dagstuhl - Leibniz-Zentrum fur Informatik

ER -

Komendantskaya E, Power J. Coalgebraic Derivations in Logic Programming. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Schloss Dagstuhl - Leibniz-Zentrum fur Informatik. 2011. p. 352-366. (Leibniz International Proceedings in Informatics (LIPIcs)). https://doi.org/10.4230/LIPIcs.CSL.2011.352