Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses

Henning Basold; Ekaterina Komendantskaya; Yue Li

doi:10.1007/978-3-030-17184-1_28

Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses

Henning Basold^*, Ekaterina Komendantskaya, Yue Li

^*Corresponding author for this work

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

12 Citations (Scopus)

52 Downloads (Pure)

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	https://doi.org/10.1007/978-3-030-17184-1_28
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
General Computer Science

Access to Document

10.1007/978-3-030-17184-1_28Licence: CC BY

Download pdfFinal published version, 1.19 MBLicence: CC BY

Cite this

@inproceedings{0e84fe97b3cc42e9a25921c40100ba5b,

title = "Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses",

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.",

keywords = "Coalgebra, Coinduction, Fibrations, Horn clause logic, Intuitionistic logic, L{\"o}b modality, Uniform proofs",

author = "Henning Basold and Ekaterina Komendantskaya and Yue Li",

year = "2019",

doi = "10.1007/978-3-030-17184-1_28",

language = "English",

isbn = "9783030171834",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "783--813",

editor = "Lu{\'i}s Caires",

booktitle = "Programming Languages and Systems",

note = "28th European Symposium on Programming 2019, ESOP 2019 ; Conference date: 06-04-2019 Through 11-04-2019",

}

Basold, H, Komendantskaya, E & Li, Y 2019, Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses. in L Caires (ed.), 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

TY - GEN

T1 - Coinduction in Uniform

T2 - 28th European Symposium on Programming 2019

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

AN - SCOPUS:85064916058

SN - 9783030171834

T3 - Lecture Notes in Computer Science

SP - 783

EP - 813

BT - Programming Languages and Systems

A2 - Caires, Luís

PB - Springer

Y2 - 6 April 2019 through 11 April 2019

ER -

Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Ekaterina Komendantskaya

Cite this

Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Profiles

Ekaterina Komendantskaya

Cite this