A Type-Theoretic Approach to Resolution

  • Peng FuEmail author
  • Ekaterina Komendantskaya
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9527)


We propose a new type-theoretic approach to SLD-resolution and Horn-clause logic programming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for the type given by the query. We propose a method of program transformation that allows to transform logic programs in such a way that proof evidence is computed alongside SLD-derivations. We discuss two applications of this approach: in recently proposed productivity theory of structural resolution, and in type class inference.


Logic programming Typed lambda calculus Realizability transformation Reduction systems Structural resolution 


  1. 1.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)CrossRefzbMATHGoogle Scholar
  2. 2.
    Bertot, Y., Komendantskaya, E.: Inductive and coinductive components of corecursive functions in coq. Electron. Notes Theor. Comput. Sci. 203(5), 25–47 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York (1989)zbMATHGoogle Scholar
  4. 4.
    Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make ad hoc proof automation less ad hoc. ACM SIGPLAN Not. 46(9), 163–175 (2011)CrossRefzbMATHGoogle Scholar
  5. 5.
    Johann, P., Komendantskaya, E., Komendantskiy, V.: Structural resolution for logic programming. In: Technical Communications, ICLP (2015)Google Scholar
  6. 6.
    Jones, M.P.: Qualified Types: Theory and Practice. Cambridge University Press, Cambridge (2003)zbMATHGoogle Scholar
  7. 7.
    Kleene, S.C.: Introduction to Metamathematics. North-Holland Publishing Company, New York (1952). Co-publisher: Wolters-Noordhoff; 8th revised ed.1980zbMATHGoogle Scholar
  8. 8.
    Komendantskaya, E., Power, J., Schmidt, M.: Coalgebraic logic programming: from semantics to implementation. J. Log. Comput. (2014)Google Scholar
  9. 9.
    Nilsson, U., Maluszynski, J.: Logic, Programming and Prolog. Wiley, Chichester (1990)zbMATHGoogle Scholar
  10. 10.
    Terese.: Term rewriting systems. In: Bezem, M., Willem Klop, J., deVrijer, R. (eds.) Cambridge Tracts in Theoretical Computer Science, vol. 55. pp. xxii + 884. Cambridge University Press (2003)Google Scholar
  11. 11.
    Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Symposium on Principles of Programming Languages, pp. 60–76. ACM (1989)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Computer ScienceUniversity of DundeeDundeeScotland

Personalised recommendations