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

1 Citation (Scopus)
18 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 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

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.

  • 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