### Abstract

We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is cast in terms of coinductive uniform proofs; its constructive content is exposed via soundness relative to an intuitionistic first-order logic with recursion controlled by the later modality; and soundness of both proof systems is proven relative to a novel coalgebraic description of complete Herbrand models.

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

Title of host publication | Programming Languages and Systems |

Subtitle of host publication | ESOP 2019 |

Editors | Luís Caires |

Publisher | Springer |

Pages | 783-813 |

Number of pages | 31 |

ISBN (Electronic) | 9783030171841 |

ISBN (Print) | 9783030171834 |

DOIs | |

Publication status | Published - 2019 |

Event | 28th European Symposium on Programming 2019 - Prague, Czech Republic Duration: 6 Apr 2019 → 11 Apr 2019 |

### Publication series

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

Publisher | Springer |

Volume | 11423 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | 28th European Symposium on Programming 2019 |
---|---|

Abbreviated title | ESOP 2019 |

Country | Czech Republic |

City | Prague |

Period | 6/04/19 → 11/04/19 |

### Fingerprint

### Keywords

- Coalgebra
- Coinduction
- Fibrations
- Horn clause logic
- Intuitionistic logic
- Löb modality
- Uniform proofs

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*Programming Languages and Systems: ESOP 2019*(pp. 783-813). (Lecture Notes in Computer Science; Vol. 11423). Springer. https://doi.org/10.1007/978-3-030-17184-1_28

}

*Programming Languages and Systems: ESOP 2019.*Lecture Notes in Computer Science, vol. 11423, Springer, pp. 783-813, 28th European Symposium on Programming 2019, Prague, Czech Republic, 6/04/19. https://doi.org/10.1007/978-3-030-17184-1_28

**Coinduction in Uniform : Foundations for Corecursive Proof Search with Horn Clauses.** / Basold, Henning; Komendantskaya, Ekaterina; Li, Yue.

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

TY - GEN

T1 - Coinduction in Uniform

T2 - Foundations for Corecursive Proof Search with Horn Clauses

AU - Basold, Henning

AU - Komendantskaya, Ekaterina

AU - Li, Yue

PY - 2019

Y1 - 2019

N2 - We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is cast in terms of coinductive uniform proofs; its constructive content is exposed via soundness relative to an intuitionistic first-order logic with recursion controlled by the later modality; and soundness of both proof systems is proven relative to a novel coalgebraic description of complete Herbrand models.

AB - We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is cast in terms of coinductive uniform proofs; its constructive content is exposed via soundness relative to an intuitionistic first-order logic with recursion controlled by the later modality; and soundness of both proof systems is proven relative to a novel coalgebraic description of complete Herbrand models.

KW - Coalgebra

KW - Coinduction

KW - Fibrations

KW - Horn clause logic

KW - Intuitionistic logic

KW - Löb modality

KW - Uniform proofs

UR - http://www.scopus.com/inward/record.url?scp=85064916058&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-17184-1_28

DO - 10.1007/978-3-030-17184-1_28

M3 - Conference contribution

SN - 9783030171834

T3 - Lecture Notes in Computer Science

SP - 783

EP - 813

BT - Programming Languages and Systems

A2 - Caires, Luís

PB - Springer

ER -