### 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 rôle 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.

Original language | English |
---|---|

Title of host publication | FLOPS 2016 |

Subtitle of host publication | Functional and Logic Programming |

Editors | Oleg Kiselyov, Andy King |

Place of Publication | Switzerland |

Publisher | Springer Verlag |

Pages | 126-143 |

Number of pages | 18 |

ISBN (Electronic) | 9783319296043 |

ISBN (Print) | 9783319296036 |

DOIs | |

Publication status | Published - 2016 |

Event | 13th International Symposium on Functional and Logic Programming, FLOPS 2016 - Kochi, Japan Duration: 4 Mar 2016 → 6 Mar 2016 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Verlag |

Volume | 9613 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | 13th International Symposium on Functional and Logic Programming, FLOPS 2016 |
---|---|

Country | Japan |

City | Kochi |

Period | 4/03/16 → 6/03/16 |

### Fingerprint

### Keywords

- Coinductive proofs
- Corecursion
- Haskell type class inference
- Horn clause logic
- Resolution

### Cite this

*FLOPS 2016: Functional and Logic Programming*(pp. 126-143). (Lecture Notes in Computer Science; Vol. 9613). Springer Verlag. https://doi.org/10.1007/978-3-319-29604-3_9