### Abstract

A propositional logic program P may be identified with a PfPf -coalgebra on the set of atomic propositions in the program. The corresponding C(P_{f}P_{f})-coalgebra, where C(P_{fPf}) 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 approach, we further extend it to arbitrary logic programs. We also exhibit a refinement of Bonchi and Zanasi’s saturation semantics for logic programming that complements lax semantics.

Original language | English |
---|---|

Title of host publication | 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 International Publishing |

Pages | 94-113 |

Number of pages | 20 |

Volume | 9608 |

ISBN (Electronic) | 9783319403700 |

ISBN (Print) | 9783319403694 |

DOIs | |

Publication status | Published - 2016 |

Event | 13th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science, CMCS 2016 Colocated with Satellite Event of the Joint Conference on Theory and Practice of Software, ETAPS 2016 - Eindhoven, Netherlands Duration: 2 Apr 2016 → 3 Apr 2016 |

### Publication series

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

Publisher | Springer International Publishing |

Volume | 9608 |

ISSN (Print) | 0302-9743 |

### Conference

Conference | 13th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science, CMCS 2016 Colocated with Satellite Event of the Joint Conference on Theory and Practice of Software, ETAPS 2016 |
---|---|

Country | Netherlands |

City | Eindhoven |

Period | 2/04/16 → 3/04/16 |

### Keywords

- Coalgebra
- Coinductive derivation tree
- Kan extensions
- Lawvere theories
- Lax transformations
- Logic programming
- Term-matching resolution

### ASJC Scopus subject areas

- Computer Science(all)
- Theoretical Computer Science

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

## Cite this

*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*(Vol. 9608, pp. 94-113). (Lecture Notes in Computer Science; Vol. 9608). Springer International Publishing. https://doi.org/10.1007/978-3-319-40370-0_7