Towards Coinductive Theory Exploration in Horn Clause Logic: Position Paper

Ekaterina Komendantskaya Dr
(Heriot-Watt University)
Yue Li
(Heriot-Watt University)

Coinduction occurs in two guises in Horn clause logic: in proofs of self-referencing properties and relations, and in proofs involving construction of (possibly irregular) infinite data. Both instances of coinductive reasoning appeared in the literature before, but a systematic analysis of these two kinds of proofs and of their relation was lacking. We propose a general proof-theoretic framework for handling both kinds of coinduction arising in Horn clause logic. To this aim, we propose a coinductive extension of Miller et al's framework of uniform proofs and prove its soundness relative to coinductive models of Horn clause logic.

In Temesghen Kahsai and German Vidal: Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2018), Oxford, UK, 13th July 2018, Electronic Proceedings in Theoretical Computer Science 278, pp. 27–33.
Published: 12th September 2018.

ArXived at: http://dx.doi.org/10.4204/EPTCS.278.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org