Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses
Logic in Computer Science
2022-03-16 v3
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.
Cite
@article{arxiv.1811.07644,
title = {Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses},
author = {Henning Basold and Ekaterina Komendantskaya and Yue Li},
journal= {arXiv preprint arXiv:1811.07644},
year = {2022}
}