Skip to main content
SpringerLink
Log in

Declarative Representation of Proof Terms

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

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.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. The Coq Development Team: The Coq proof assistant reference manual (2005)

  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)

    Article  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  5. Guidi, F.: Procedural representation of CIC proof terms. J. Autom. Reason. (2009). doi:10.1007/s10817-009-9137-6

  6. Raffalli, C.: The proof checker documentation, version 0.85, manual of the PhoX proof assistant (2005)

  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)

    Chapter  Google Scholar 

  8. Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Autom. Reason. 29(3–4), 389–411 (2002)

    Article  MATH  MathSciNet  Google Scholar 

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

  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

    Chapter  Google Scholar 

  13. Kirchner, F., Sacerdoti Coen, C.: The Fellowship Super-prover. http://www.lix.polytechnique.fr/Labo/Florent.Kirchner/fellowship/ (2008)

  14. Kirchner, F.: Interoperable proof systems. Ph.D. thesis, École Polytechnique (2007)

  15. Asperti, A., Loeb, I., Sacerdoti Coen, C.: Stylesheets to intermediate representation and presentational stylesheets. MoWGLI Report D2d,D2f (2003)

  16. Asperti, A., Tassi, E.: An interactive driver for goal directed proof strategies. In: Proc. of User Interfaces for Theorem Provers 2008, Montreal (2008)

  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)

  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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Scienze dell’Informazione, via Mura Anteo Zamboni n. 7, 40127, Bologna, Italy

    Claudio Sacerdoti Coen

Authors
  1. Claudio Sacerdoti Coen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Claudio Sacerdoti Coen.

Additional information

Partially supported by the Strategic Project DAMA (Dimostrazione Assistita per la Matematica e l’Apprendimento) of the University of Bologna.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Sacerdoti Coen, C. Declarative Representation of Proof Terms. J Autom Reasoning 44, 25 (2010). https://doi.org/10.1007/s10817-009-9136-7

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s10817-009-9136-7

Keywords

Search

Navigation