2019/03/18 by Ekaterina Komendantskaya, Yue Li, Komendantskaya, Ekaterina +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1903.07371
openalex publication_date 2019/03/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Coinduction occurs in two guises in Horn clause logic: in proofs of circular properties and relations, and in proofs involving construction of 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 framework of uniform proofs and prove its soundness relative to coinductive models of Horn clause logic.