Skip to main content
SpringerLink
Log in

Proof Checking and Logic Programming

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

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

Abstract

In a world where trusting software systems is increasingly important, formal methods and formal proof can help provide trustable foundations. Proof checking can help to reduce the size of the trusted base since we do not need to trust an entire theorem prover if we can check the proofs they produce by a trusted (and smaller) checker. Many approaches to building proof checkers require embedding within them a full programming language. In most many modern proof checkers and theorem provers, that programming language is a functional programming language, often a variant of ML. In fact, parts of ML (e.g., strong typing, abstract datatypes, and higher-order programming) were designed to make ML into a trustworthy “meta-language” for checking proofs. While there is considerable overlap in the foundations of logic programming and proof checking (both benefit from unification, backtracking search, efficient term structures, etc.), the discipline of logic programming has, in fact, played a minor role in the history of proof checking. I will argue that logic programming can have a major role in the future of this important topic.

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.

    Some specialized theorem provers related to SAT solving have adopted standards of outputting their proof evidence (see, for example, [36]).

References

  1. Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297–347 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  2. Assaf, A.: A framework for defining computational higher-order logics. Ph.D. thesis, École Polytechnique, September 2015

    Google Scholar 

  3. Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: a system for reasoning about relational specifications. J. Formalized Reason. 7(2), 1–89 (2014)

    MathSciNet  Google Scholar 

  4. Blanco, R., Miller, D.: Proof outlines as proof certificates: a system description. Draft available online, September 2015

    Google Scholar 

  5. Boyer, R.S., Moore, J.S., San Diego: A Computational Logic. Academic Press, San Diego (1979)

    Google Scholar 

  6. Chaudhuri, K., Pfenning, F., Price, G.: A logical characterization of forward and backward chaining in the inverse method. J. Autom. Reason. 40(2–3), 133–177 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  7. Chihani, Z., Miller, D., Renaud, F.: Foundational proof certificates in first-order logic. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 162–177. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  8. Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56–68 (1940)

    Article  MathSciNet  MATH  Google Scholar 

  9. Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-Pi-calculus modulo. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 102–117. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Danos, V., Joinet, J.B., Schellinx, H.: LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In: Girard, J.-Y., Lafont, Y., Regnier, L., (eds.) Advances in Linear Logic. London Mathematical Society Lecture Note Series, vol. 22, pp. 211–224. Cambridge University Press (1995)

    Google Scholar 

  11. The Dedukti system (2013). https://www.rocq.inria.fr/deducteam/Dedukti/index.html

  12. Dunchev, C., Guidi, F., Coen, C.S., Tassi, E.; A fast interpreter for \(\lambda \)Prolog. In: International Conference on LPAR-20: Logic Programming and Automated Reasoning (2015) (to appear)

    Google Scholar 

  13. Dyckhoff, R., Lengrand, S.: Call-by-value \(\lambda \)-calculus and LJQ. J. Logic Comput. 17(6), 1109–1134 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  14. Gacek, A., Miller, D., Nadathur, G.: A two-level logic approach to reasoning about computations. J. Autom. Reason. 49(2), 241–273 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  15. Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68–131, North-Holland, Amsterdam (1935)

    Google Scholar 

  16. Girard, J.-Y.: Linear logic. Theo. Comput. Sci. 50, 1–102 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  17. Girard, J.-Y.: A new constructive logic: classical logic. Math. Struct. Comp. Sci. 1, 255–296 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  18. Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, pp. 333–333. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  19. Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979)

    MATH  Google Scholar 

  20. Hales, T.C.: A proof of the Kepler conjecture. Ann. Math. 162(3), 1065–1185 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  21. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  22. Herbelin, H.: Séquents qu’on calcule: de l’interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes. Ph.D. thesis, Université Paris 7 (1995)

    Google Scholar 

  23. Howe, J.M., Proof search issues in some non-classical logics. Ph.D. thesis, University of St Andrews. Available as University of St Andrews Research Report CS/99/1, December 1998

    Google Scholar 

  24. Klein, G., Elphinstone, K., Heiser, G., Andronick, D., Cock, P., Derrin, D., Elkaduwe, K., Engelhardt, R., Kolanski, M., Norrish, T., Tuch, S.T., Winwood, S.: seL4: Formal verification of an OS kernel. In Proceedings of the 22nd Symposium on Operating Systems Principles (22nd SOSP 2009), Operating Systems Review (OSR), pp. 207–220, Big Sky, MT. ACM SIGOPS, October 2009

    Google Scholar 

  25. Laurent, O.: Etude de la polarisation en logique. Ph.D. thesis, Université Aix-Marseille II, March 2002

    Google Scholar 

  26. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  27. Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theo. Comput. Sci. 410(46), 4747–4768 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  28. Meng, J.: The integration of higher order interactive proof with first order automatic theorem proving. Ph.D. thesis, University of Cambridge, Computer Laboratory (2015)

    Google Scholar 

  29. Miller, D.: Abstractions in logic programming. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 329–359. Academic Press, San Diego (1990)

    Google Scholar 

  30. Miller, D.: Communicating and trusting proofs: the case for broad spectrum proof certificates. In: Proceedings of the Fourteenth International Congress on Logic, Methodology, and Philosophy of Science, pp. 323–342. College Publications (2014)

    Google Scholar 

  31. Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)

    Book  MATH  Google Scholar 

  32. Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Logic 51, 125–157 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  33. Nadathur, G., Mitchell, D.J.: System description: Teyjus - a compiler and abstract machine based implementation of \(\lambda \)Prolog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287–291. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  34. Pereira, F.: C-Prolog User’s Manual, Version 1.5, June 1988

    Google Scholar 

  35. Pfenning, F., Schürmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  36. Wetzler, N., Heule, M.J.H., Hunt Jr, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Heidelberg (2014)

    Google Scholar 

Download references

Acknowledgments

Zak Chihani provided comments on an earlier version of this paper. The work presented here has been funded by the ERC Advanced GrantProofCert.

Author information

Authors and Affiliations

  1. Inria and LIX/École Polytechnique, Palaiseau, France

    Dale Miller

Authors
  1. Dale Miller
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dale Miller .

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

Miller, D. (2015). Proof Checking and Logic Programming. 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_1

Download citation

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

  • 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