Coinduction in uniform: foundations for corecursive proof search with Horn clauses
From MaRDI portal
Publication:6070807
DOI10.1007/978-3-030-17184-1_28zbMATH Open1524.68183arXiv1811.07644MaRDI QIDQ6070807
Yue Li, Ekaterina Komendantskaya, Henning Basold
Publication date: 24 November 2023
Published in: Programming Languages and Systems (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1811.07644
Related Items (3)
Strategy of searching of a conclusion in Horn clauses with unitary consideration of sub-target ⋮ Checking equivalence of corecursive streams: an inductive procedure ⋮ Reducing higher-order recursion scheme equivalence to coinductive higher-order constrained Horn clauses
This page was built for publication: Coinduction in uniform: foundations for corecursive proof search with Horn clauses
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6070807)
