Towards Coinductive Theory Exploration in Horn Clause Logic: Position Paper
This work addresses foundational issues in automated theorem proving and logic programming, but it is incremental as it builds on existing frameworks like uniform proofs.
The paper tackles the lack of systematic analysis of coinductive reasoning in Horn clause logic by proposing a general proof-theoretic framework that handles both self-referencing properties and infinite data constructions, and proves its soundness relative to coinductive models.
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.