A Proposal for Broad Spectrum Proof Certificates

  • Dale Miller
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7086)


Recent developments in the theory of focused proof systems provide flexible means for structuring proofs within the sequent calculus. This structuring is organized around the construction of “macro” level inference rules based on the “micro” inference rules which introduce single logical connectives. After presenting focused proof systems for first-order classical logics (one with and one without fixed points and equality) we illustrate several examples of proof certificates formats that are derived naturally from the structure of such focused proof systems. In principle, a proof certificate contains two parts: the first part describes how macro rules are defined in terms of micro rules and the second part describes a particular proof object using the macro rules. The first part, which is based on the vocabulary of focused proof systems, describes a collection of macro rules that can be used to directly present the structure of proof evidence captured by a particular class of computational logic systems. While such proof certificates can capture a wide variety of proof structures, a proof checker can remain simple since it must only understand the micro-rules and the discipline of focusing. Since proofs and proof certificates are often likely to be large, there must be some flexibility in allowing proof certificates to elide subproofs: as a result, proof checkers will necessarily be required to perform (bounded) proof search in order to reconstruct missing subproofs. Thus, proof checkers will need to do unification and restricted backtracking search.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. of Logic and Computation 2(3), 297–347 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Andrews, P.B.: Theorem-proving via general matings. J. ACM 28, 193–214 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Appel, A.W., Felty, A.P.: Polymorphic lemmas and definitions in λProlog and Twelf. Theory and Practice of Logic Programming 4(1-2), 1–39 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Baelde, D.: A linear approach to the proof-theory of least and greatest fixed points. PhD thesis, Ecole Polytechnique (December 2008)Google Scholar
  5. 5.
    Baelde, D.: Least and greatest fixed points in linear logic. Accepted to the ACM Transactions on Computational Logic (September 2010)Google Scholar
  6. 6.
    Baelde, D., Miller, D., Snow, Z.: Focused Inductive Theorem Proving. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 278–292. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  7. 7.
    Barendregt, H.: Lambda calculus with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 117–309. Oxford University Press (1992)Google Scholar
  8. 8.
    Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. J. of Automated Reasoning 28(3), 321–336 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Boespflug, M.: Conception d’un noyau de vérification de preuves pour le λΠ-calcul modulo. PhD thesis, Ecole Polytechnique (2011)Google Scholar
  10. 10.
    Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. of Automated Reasoning 31(1), 31–72 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Gentzen, G.: Investigations into logical deductions. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam (1969); Translation of articles that appeared in 1934-1935Google Scholar
  12. 12.
    Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science 410(46), 4747–4768 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Liang, C., Miller, D.: Kripke semantics and proof systems for combining intuitionistic logic and classical logic (September 2011) (submitted)Google Scholar
  14. 14.
    Martin-Löf, P.: Constructive mathematics and computer programming. In: Sixth International Congress for Logic, Methodology, and Philosophy of Science, Amsterdam, pp. 153–175. North-Holland (1982)Google Scholar
  15. 15.
    Miller, D.: Communicating and trusting proofs: The case for broad spectrum proof certificates (June 2011); Available from author’s websiteGoogle Scholar
  16. 16.
    Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51, 125–157 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Miller, D., Nigam, V.: Incorporating Tables into Proofs. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 466–480. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. 18.
    Nadathur, G., Mitchell, D.J.: System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of λProlog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287–291. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  19. 19.
    Necula, G.C.: Proof-carrying code. In: Conference Record of the 24th Symposium on Principles of Programming Languages 1997, Paris, France, pp. 106–119. ACM Press (1997)Google Scholar
  20. 20.
    Pratt, V.R.: Every prime has a succinct certificate. SIAM Journal on Computing 4(3), 214–220 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Shankar, N.: Trust and Automation in Verification Tools. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 4–17. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Dale Miller
    • 1
  1. 1.INRIA & LIX, École PolytechniqueFrance

Personalised recommendations