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 proceedingConference contribution

11 Citations (Scopus)
28 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
Country/TerritoryCzech 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