Proof relevant corecursive resolution

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

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

11 Citations (Scopus)

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 languageEnglish
Title of host publicationFLOPS 2016
Subtitle of host publicationFunctional and Logic Programming
EditorsOleg Kiselyov, Andy King
Place of PublicationSwitzerland
PublisherSpringer Verlag
Pages126-143
Number of pages18
ISBN (Electronic)9783319296043
ISBN (Print)9783319296036
DOIs
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
Volume9613
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference13th International Symposium on Functional and Logic Programming, FLOPS 2016
CountryJapan
CityKochi
Period4/03/166/03/16

    Fingerprint

Keywords

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

Cite this

Fu, P., Komendantskaya, E., Schrijvers, T., & Pond, A. (2016). Proof relevant corecursive resolution. In O. Kiselyov, & A. King (Eds.), 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