Advertisement

Proof Checking and Logic Programming

  • Dale MillerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

Keywords

Proof Checker Abstract Datatype Theorem Prover Focused Proof System Credible Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Notes

Acknowledgments

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

References

  1. 1.
    Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297–347 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Assaf, A.: A framework for defining computational higher-order logics. Ph.D. thesis, École Polytechnique, September 2015Google Scholar
  3. 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)MathSciNetGoogle Scholar
  4. 4.
    Blanco, R., Miller, D.: Proof outlines as proof certificates: a system description. Draft available online, September 2015Google Scholar
  5. 5.
    Boyer, R.S., Moore, J.S., San Diego: A Computational Logic. Academic Press, San Diego (1979)Google Scholar
  6. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 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) CrossRefGoogle Scholar
  8. 8.
    Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56–68 (1940)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 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) CrossRefGoogle Scholar
  10. 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. 11.
  12. 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. 13.
    Dyckhoff, R., Lengrand, S.: Call-by-value \(\lambda \)-calculus and LJQ. J. Logic Comput. 17(6), 1109–1134 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Gacek, A., Miller, D., Nadathur, G.: A two-level logic approach to reasoning about computations. J. Autom. Reason. 49(2), 241–273 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 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. 16.
    Girard, J.-Y.: Linear logic. Theo. Comput. Sci. 50, 1–102 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Girard, J.-Y.: A new constructive logic: classical logic. Math. Struct. Comp. Sci. 1, 255–296 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 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) CrossRefGoogle Scholar
  19. 19.
    Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979)zbMATHGoogle Scholar
  20. 20.
    Hales, T.C.: A proof of the Kepler conjecture. Ann. Math. 162(3), 1065–1185 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 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. 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 1998Google Scholar
  24. 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 2009Google Scholar
  25. 25.
    Laurent, O.: Etude de la polarisation en logique. Ph.D. thesis, Université Aix-Marseille II, March 2002Google Scholar
  26. 26.
    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRefGoogle Scholar
  27. 27.
    Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theo. Comput. Sci. 410(46), 4747–4768 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 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. 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. 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. 31.
    Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)CrossRefzbMATHGoogle Scholar
  32. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  33. 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) CrossRefGoogle Scholar
  34. 34.
    Pereira, F.: C-Prolog User’s Manual, Version 1.5, June 1988Google Scholar
  35. 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) CrossRefGoogle Scholar
  36. 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

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Inria and LIX/École PolytechniquePalaiseauFrance

Personalised recommendations