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

3 Citations (Scopus)
19 Downloads (Pure)


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
Number of pages31
ISBN (Electronic)9783030171841
ISBN (Print)9783030171834
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
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference28th European Symposium on Programming 2019
Abbreviated titleESOP 2019
CountryCzech Republic


  • 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