Abstract
We consider an extension of OMDoc proofs with alternative sub-proofs and proofs at different level of detail, and an affine non-deterministic fragment of the \({\overline{\lambda}\mu\tilde{\mu}}\)-calculus seen as a proof format. We provide explanations in pseudo-natural language of proofs in both formats, and a formal correspondence between the two by means of two mutually inverse encodings of one format in the other one.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Autexier, S., Benzmüller, C., Dietrich, D., Meier, A., Wirth, C.: A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, Springer, Heidelberg (2006)
Curien, P., Herbelin, H.: The duality of computation. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP 2000). SIGPLAN Notices, vol. 35(9), pp. 233–243. ACM, New York (2000)
Kohlhase, M.: OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2)
Sacerdoti Coen, C.: Explanation in Natural language of terms. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, Springer, Heidelberg (2006)
Wiedijk, F.: Formal Proof Sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 378–393. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Autexier, S., Sacerdoti-Coen, C. (2006). A Formal Correspondence Between OMDoc with Alternative Proofs and the \({\overline{\lambda}\mu\tilde{\mu}}\)-Calculus. In: Borwein, J.M., Farmer, W.M. (eds) Mathematical Knowledge Management. MKM 2006. Lecture Notes in Computer Science(), vol 4108. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11812289_7
Download citation
DOI: https://doi.org/10.1007/11812289_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37104-5
Online ISBN: 978-3-540-37106-9
eBook Packages: Computer ScienceComputer Science (R0)