2015/11/30 by Peng Fu, Fu, Peng, Ekaterina Komendantskaya +5
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 #cs.LO
paper · pdf · doi:10.48550/arxiv.1511.09394
23 pages, with appendices in FLOPS 2016
arxiv created 2015/11/30 · openalex publication_date 2015/11/30 · arxiv updated 2015/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Resolution lies at the foundation of both logic programming and type class context reduction in functional languages. Terminating derivations by resolution have well-defined inductive meaning, whereas some non-terminating derivations can be understood coinductively. Cycle detection is a popular method to capture a small subset of such derivations. We show that in fact cycle detection is a restricted form of coinductive proof, in which the atomic formula forming the cycle plays the role of coinductive hypothesis. This paper introduces a heuristic method for obtaining richer coinductive hypotheses in the form of Horn formulas. Our approach subsumes cycle detection and gives coinductive meaning to a larger class of derivations. For this purpose we extend resolution with Horn formula resolvents and corecursive evidence generation. We illustrate our method on non-terminating type class resolution problems.