Research

Category theoretic semantics for theorem proving in logic programming: embracing the laxness


Reference:

Komendantskaya, E. and Power, J., 2016. Category theoretic semantics for theorem proving in logic programming: embracing the laxness. Springer, pp. 94-113. (Lecture Notes in Computer Science)

Related documents:

[img]
Preview
PDF (finalaccepted) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (360kB) | Preview

    Official URL:

    http://dx.doi.org/10.1007/978-3-319-40370-0_7

    Abstract

    A propositional logic program P may be identified with a P f P f -coalgebra on the set of atomic propositions in the program. The corresponding C(P f P f )-coalgebra, where C(P f P f ) is the cofree comonad on P f P f , describes derivations by resolution. Using lax semantics, that correspondence may be extended to a class of first-order logic programs without existential variables. The resulting extension captures the proofs by term-matching resolution in logic programming. Refining the lax ap- proach, we further extend it to arbitrary logic programs. We also exhibit a refinement of Bonchi and Zanasi’s saturation semantics for logic pro- gramming that complements lax semantics.

    Details

    Item Type Conference or Workshop Items (UNSPECIFIED)
    CreatorsKomendantskaya, E.and Power, J.
    EditorsHasuo, I.
    DOI10.1007/978-3-319-40370-0_7
    Uncontrolled Keywordslogic programming, coalgebra, term-matching resolution, coinductive derivation tree, lawvere theories, lax transformations, kan extensions.
    DepartmentsFaculty of Science > Computer Science
    Publisher Statement12feb16version.pdf: The final publication is available at Springer via http://dx.doi.org/[insert DOI]”.
    StatusPublished
    ID Code49979

    Export

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...