### Abstract

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.

Language | English |
---|---|

Title of host publication | Proceedings of Coalgebraic Methods in Computer Science |

Subtitle of host publication | 13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers |

Editors | Ichiro Hasuo |

Publisher | Springer |

Pages | 94-113 |

ISBN (Print) | 9783319403694 |

DOIs | |

Status | Published - 4 Jun 2016 |

### Publication series

Name | Lecture Notes in Computer Science |
---|

Name | |
---|---|

Volume | 9608 |

### Fingerprint

### Keywords

- Logic programming, coalgebra, term-matching resolution, coinductive derivation tree, Lawvere theories, lax transformations, Kan extensions.

### Cite this

*Proceedings of Coalgebraic Methods in Computer Science: 13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers*(pp. 94-113). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-319-40370-0_7

**Category theoretic semantics for theorem proving in logic programming: embracing the laxness.** / Komendantskaya, Ekaterina ; Power, John.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Proceedings of Coalgebraic Methods in Computer Science: 13th IFIP WG 1.3 International Workshop, CMCS 2016, Colocated with ETAPS 2016, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers.*Lecture Notes in Computer Science, Springer, pp. 94-113. https://doi.org/10.1007/978-3-319-40370-0_7

}

TY - GEN

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

AU - Komendantskaya, Ekaterina

AU - Power, John

PY - 2016/6/4

Y1 - 2016/6/4

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

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

KW - Logic programming, coalgebra, term-matching resolution, coinductive derivation tree, Lawvere theories, lax transformations, Kan extensions.

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

U2 - 10.1007/978-3-319-40370-0_7

DO - 10.1007/978-3-319-40370-0_7

M3 - Conference contribution

SN - 9783319403694

T3 - Lecture Notes in Computer Science

SP - 94

EP - 113

BT - Proceedings of Coalgebraic Methods in Computer Science

A2 - Hasuo, Ichiro

PB - Springer

ER -