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

Henning Basold, Ekaterina Komendantskaya, Yue Li

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

LanguageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publicationESOP 2019
EditorsLuís Caires
PublisherSpringer
Pages783-813
Number of pages31
ISBN (Electronic)9783030171841
ISBN (Print)9783030171834
DOIs
Publication statusPublished - 2019
Event28th European Symposium on Programming 2019 - Prague, Czech Republic
Duration: 6 Apr 201911 Apr 2019

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume11423
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference28th European Symposium on Programming 2019
Abbreviated titleESOP 2019
CountryCzech Republic
CityPrague
Period6/04/1911/04/19

Fingerprint

Coinduction
Proof Search
Horn clause
Soundness
Semantics
Intuitionistic Logic
Proof System
Operational Semantics
First-order Logic
Recursion
Modality
Model

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

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 (pp. 783-813). (Lecture Notes in Computer Science; Vol. 11423). Springer. https://doi.org/10.1007/978-3-030-17184-1_28
Basold, Henning ; Komendantskaya, Ekaterina ; Li, Yue. / Coinduction in Uniform : Foundations for Corecursive Proof Search with Horn Clauses. Programming Languages and Systems: ESOP 2019. editor / Luís Caires. Springer, 2019. pp. 783-813 (Lecture Notes in Computer Science).
@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",

}

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

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

Programming Languages and Systems: ESOP 2019. ed. / Luís Caires. Springer, 2019. p. 783-813 (Lecture Notes in Computer Science; Vol. 11423).

Research output: Chapter in Book/Report/Conference proceedingConference 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 -

Basold H, Komendantskaya E, Li Y. Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses. In Caires L, editor, Programming Languages and Systems: ESOP 2019. Springer. 2019. p. 783-813. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-17184-1_28