Proof relevant corecursive resolution

Peng Fu (Lead / Corresponding author), Ekaterina Komendantskaya, Tom Schrijvers, Andrew Pond

Research output: Chapter in Book/Report/Conference proceedingConference contribution

20 Citations (Scopus)


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 languageEnglish
Title of host publicationFLOPS 2016
Subtitle of host publicationFunctional and Logic Programming
EditorsOleg Kiselyov, Andy King
Place of PublicationSwitzerland
PublisherSpringer Verlag
Number of pages18
ISBN (Electronic)9783319296043
ISBN (Print)9783319296036
Publication statusPublished - 2016
Event13th International Symposium on Functional and Logic Programming, FLOPS 2016 - Kochi, Japan
Duration: 4 Mar 20166 Mar 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference13th International Symposium on Functional and Logic Programming, FLOPS 2016


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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Proof relevant corecursive resolution'. Together they form a unique fingerprint.

Cite this