Proof Relevant Corecursive Resolution

TL;DR

This paper presents a novel method that extends resolution with Horn formulas and corecursive evidence, enabling richer coinductive reasoning and capturing a broader class of non-terminating derivations in logic programming.

Contribution

It introduces a heuristic for generating richer coinductive hypotheses using Horn formulas, extending cycle detection to more derivations in resolution.

Findings

Subsumes cycle detection as a special case

Enables coinductive reasoning for larger classes of derivations

Improves understanding of non-terminating type class resolution

Abstract

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.