# Proof Relevant Corecursive Resolution

arXiv: https://arxiv.org/abs/1511.09394 · HTML: https://mlsanity.com/paper/1511.09394/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Nov 2015.

## Built on by (most cited first, 1 of 1)

- [Actions You Can Handle: Dependent Types for AI Plans](https://mlsanity.com/paper/2105.11267/) (2021)

## Abstract (arXiv)

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.