Skip to main content
SpringerLink
Log in

A Type-Theoretic Approach to Resolution

  • Conference paper
  • First Online:
Logic-Based Program Synthesis and Transformation (LOPSTR 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9527))

Abstract

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.

This work was funded by EPSRC grant EP/K031864/1.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Extended version is available at both authors’ homepages.

References

  1. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)

    Book  MATH  Google Scholar 

  2. Bertot, Y., Komendantskaya, E.: Inductive and coinductive components of corecursive functions in coq. Electron. Notes Theor. Comput. Sci. 203(5), 25–47 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  3. Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York (1989)

    MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  5. Johann, P., Komendantskaya, E., Komendantskiy, V.: Structural resolution for logic programming. In: Technical Communications, ICLP (2015)

    Google Scholar 

  6. Jones, M.P.: Qualified Types: Theory and Practice. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  7. Kleene, S.C.: Introduction to Metamathematics. North-Holland Publishing Company, New York (1952). Co-publisher: Wolters-Noordhoff; 8th revised ed.1980

    MATH  Google Scholar 

  8. Komendantskaya, E., Power, J., Schmidt, M.: Coalgebraic logic programming: from semantics to implementation. J. Log. Comput. (2014)

    Google Scholar 

  9. Nilsson, U., Maluszynski, J.: Logic, Programming and Prolog. Wiley, Chichester (1990)

    MATH  Google Scholar 

  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. 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 

Download references

Author information

Authors and Affiliations

  1. Computer Science, University of Dundee, Dundee, Scotland

    Peng Fu & Ekaterina Komendantskaya

Authors
  1. Peng Fu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ekaterina Komendantskaya
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peng Fu .

Editor information

Editors and Affiliations

  1. Università di Siena, Siena, Italy

    Moreno Falaschi

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Fu, P., Komendantskaya, E. (2015). A Type-Theoretic Approach to Resolution. In: Falaschi, M. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2015. Lecture Notes in Computer Science(), vol 9527. Springer, Cham. https://doi.org/10.1007/978-3-319-27436-2_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-27436-2_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-27435-5

  • Online ISBN: 978-3-319-27436-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation