| Autor: |
Basold, Henning, Komendantskaya, Ekaterina, Li, Yue |
| Rok vydání: |
2018 |
| Předmět: |
|
| Zdroj: |
LNCS 11423 (2019) 783-813 |
| Druh dokumentu: |
Working Paper |
| DOI: |
10.1007/978-3-030-17184-1_28 |
| Popis: |
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. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
