Projects per year

### 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.

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.

Original 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 |

Number of pages | 20 |

ISBN (Print) | 9783319403694 |

DOIs | |

Publication status | Published - 4 Jun 2016 |

### Publication series

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

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

Name | |
---|---|

Volume | 9608 |

### Keywords

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

## Fingerprint Dive into the research topics of 'Category theoretic semantics for theorem proving in logic programming: embracing the laxness'. Together they form a unique fingerprint.

## Projects

- 1 Finished

### Coalgebraic Logic Programming for Type Inference

Power, J.

Engineering and Physical Sciences Research Council

1/09/13 → 31/01/17

Project: Research council

## Cite this

Komendantskaya, E., & Power, J. (2016). Category theoretic semantics for theorem proving in logic programming: embracing the laxness. In I. Hasuo (Ed.),

*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