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.
Original 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/Territory | Czech Republic |
City | Prague |
Period | 6/04/19 → 11/04/19 |
Keywords
- Coalgebra
- Coinduction
- Fibrations
- Horn clause logic
- Intuitionistic logic
- Löb modality
- Uniform proofs
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)
Fingerprint
Dive into the research topics of 'Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses'. Together they form a unique fingerprint.Profiles
-
Ekaterina Komendantskaya
- School of Mathematical & Computer Sciences - Professor
- School of Mathematical & Computer Sciences, Computer Science - Professor
Person: Academic (Research & Teaching)