### Abstract

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

Title of host publication | Algebra and Coalgebra in Computer Science |

Subtitle of host publication | 4th International Conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings |

Editors | Andrea Corradini, Bartek Klin, Corina Cîrstea |

Publisher | Springer |

Pages | 268-282 |

Number of pages | 15 |

ISBN (Electronic) | 9783642229442 |

ISBN (Print) | 9783642229435 |

DOIs | |

Publication status | Published - 2011 |

### Publication series

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

Publisher | Springer Berlin Heidelberg |

Volume | 6859 |

ISSN (Print) | 0302-9743 |

### Fingerprint

### Keywords

- Logic programming
- SLD-resolution
- Coalgebra
- Lawvere theories
- Lax natural transformations
- Oplax maps of coalgebras

### Cite this

*Algebra and Coalgebra in Computer Science: 4th International Conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings*(pp. 268-282). (Lecture Notes in Computer Science; Vol. 6859). Springer. https://doi.org/10.1007/978-3-642-22944-2_19

}

*Algebra and Coalgebra in Computer Science: 4th International Conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings.*Lecture Notes in Computer Science, vol. 6859, Springer, pp. 268-282. https://doi.org/10.1007/978-3-642-22944-2_19

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

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

TY - CHAP

T1 - Coalgebraic Semantics for Derivations in Logic Programming

AU - Komendantskaya, Ekaterina

AU - Power, John

PY - 2011

Y1 - 2011

N2 - Every variable-free logic program induces a P P -coalgebra on the set of atomic formulae in the program. The coalgebra p sends an atomic formula A to the set of the sets of atomic formulae in the antecedent of each clause for which A is the head. In an earlier paper, we identified a variable-free logic program with a P P -coalgebra on Set and showed that, if C(P P ) is the cofree comonad on P P , then given a logic program P qua P P -coalgebra, the corresponding C(P P )-coalgebra structure describes the parallel and-or derivation trees of P. In this paper, we extend that analysis to arbitrary logic programs. That requires a subtle analysis of lax natural transformations between Poset-valued functors on a Lawvere theory, of locally ordered endofunctors and comonads on locally ordered categories, and of coalgebras, oplax maps of coalgebras, and the relationships between such for locally ordered endofunctors and the cofree comonads on them.

AB - Every variable-free logic program induces a P P -coalgebra on the set of atomic formulae in the program. The coalgebra p sends an atomic formula A to the set of the sets of atomic formulae in the antecedent of each clause for which A is the head. In an earlier paper, we identified a variable-free logic program with a P P -coalgebra on Set and showed that, if C(P P ) is the cofree comonad on P P , then given a logic program P qua P P -coalgebra, the corresponding C(P P )-coalgebra structure describes the parallel and-or derivation trees of P. In this paper, we extend that analysis to arbitrary logic programs. That requires a subtle analysis of lax natural transformations between Poset-valued functors on a Lawvere theory, of locally ordered endofunctors and comonads on locally ordered categories, and of coalgebras, oplax maps of coalgebras, and the relationships between such for locally ordered endofunctors and the cofree comonads on them.

KW - Logic programming

KW - SLD-resolution

KW - Coalgebra

KW - Lawvere theories

KW - Lax natural transformations

KW - Oplax maps of coalgebras

U2 - 10.1007/978-3-642-22944-2_19

DO - 10.1007/978-3-642-22944-2_19

M3 - Chapter

SN - 9783642229435

T3 - Lecture Notes in Computer Science

SP - 268

EP - 282

BT - Algebra and Coalgebra in Computer Science

A2 - Corradini, Andrea

A2 - Klin, Bartek

A2 - Cîrstea, Corina

PB - Springer

ER -