Advertisement

Declarative Representation of Proof Terms

  • Claudio Sacerdoti Coen
Article

Abstract

We present a declarative language inspired by the pseudo-natural language previously used in Matita for the explanation of proof terms. We show how to compile the language to proof terms and how to automatically generate declarative scripts from proof terms. Then we investigate the relationship between the two translations, identifying the amount of proof structure preserved by compilation and re-generation of declarative scripts.

Keywords

Declarative language Proof terms Translation Generation 

References

  1. 1.
    The Coq Development Team: The Coq proof assistant reference manual (2005)Google Scholar
  2. 2.
    Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. J. Autom. Reason. 39(2), 109–139 (2007)MATHCrossRefGoogle Scholar
  3. 3.
    Sacerdoti Coen, C.: Explanation in natural language of lambda-bar-mu-mu-tilde-terms. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) Post-Proceedings of the Fourth International Conference on Mathematical Knowledge Management, MKM 2005. Lecture Notes in Computer Science, vol. 3863, pp. 234–249. Springer, New York (2006)Google Scholar
  4. 4.
    Autexier, S., Sacerdoti Coen, C.: A formal correspondence between omdoc with alternative proofs and the lambda-bar-mu-mu-tilde-calculus. In: Proceedings of Mathematical Knowledge Management 2006. Lectures Notes in Artificial Intelligence, vol. 4108, pp. 67–81. Springer, New York (2006)CrossRefGoogle Scholar
  5. 5.
    Guidi, F.: Procedural representation of CIC proof terms. J. Autom. Reason. (2009). doi: 10.1007/s10817-009-9137-6
  6. 6.
    Raffalli, C.: The proof checker documentation, version 0.85, manual of the PhoX proof assistant (2005)Google Scholar
  7. 7.
    Wenzel, M.: Isar—a generic interpretative approach to readable formal proof documents. In: Theorem Proving in Higher Order Logics. LNCS, vol. 1690, pp. 167–184. Springer, New York (1999)CrossRefGoogle Scholar
  8. 8.
    Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Autom. Reason. 29(3–4), 389–411 (2002)MATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: Tinycals: step by step tacticals. In: Proceedings of User Interface for Theorem Provers 2006. Electronic Notes in Theoretical Computer Science, vol. 174, pp. 125–142. Elsevier, Amsterdam (2006)Google Scholar
  10. 10.
    Harrison, J.: A Mizar mode for HOL. In: von Wright, J., Grundy, J., Harrison, J. (eds.) Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs’96. LNCS, vol. 1125, pp. 203–220. Springer, New York (1996)Google Scholar
  11. 11.
    Sacerdoti Coen, C.: Tactics in modern proof-assistants: the bad habit of overkilling. In: Supplementary Proceedings of the 14th International Conference TPHOLS 2001, pp. 352–367 (2001)Google Scholar
  12. 12.
    Curien, P.L., Herbelin, H.: The duality of computation. In: ICFP ’00: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pp. 233–243. ACM, New York (2000). doi:http://doi.acm.org/10.1145/351240.351262 CrossRefGoogle Scholar
  13. 13.
    Kirchner, F., Sacerdoti Coen, C.: The Fellowship Super-prover. http://www.lix.polytechnique.fr/Labo/Florent.Kirchner/fellowship/ (2008)
  14. 14.
    Kirchner, F.: Interoperable proof systems. Ph.D. thesis, École Polytechnique (2007)Google Scholar
  15. 15.
    Asperti, A., Loeb, I., Sacerdoti Coen, C.: Stylesheets to intermediate representation and presentational stylesheets. MoWGLI Report D2d,D2f (2003)Google Scholar
  16. 16.
    Asperti, A., Tassi, E.: An interactive driver for goal directed proof strategies. In: Proc. of User Interfaces for Theorem Provers 2008, Montreal (2008)Google Scholar
  17. 17.
    Coscoy, Y., Kahn, G., Thery, L.: Extracting text from proofs. Technical Report RR-2459, Inria (Institut National de Recherche en Informatique et en Automatique), France (1995)Google Scholar
  18. 18.
    Corbineau, P.: A declarative proof language for the Coq proof assistant. In: TYPES 2007: Types for Proof and Programs. LNCS, vol. 4941. Springer, New York (2008)CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media B.V. 2009

Authors and Affiliations

  1. 1.Dipartimento di Scienze dell’Informazionevia Mura Anteo Zamboni n. 7BolognaItaly

Personalised recommendations