Abstract
There are two different styles for writing natural deduction proofs: the ‘Gentzen’ style in which a proof is a tree with the conclusion at the root and the assumptions at the leaves, and the ‘Fitch’ style (also called ‘flag’ style) in which a proof consists of lines that are grouped together in nested boxes.
In the world of proof assistants these two kinds of natural deduction correspond to procedural proofs (tactic scripts that work on one or more subgoals, like those of the Coq, HOL and PVS systems), and declarative proofs (like those of the Mizar and Isabelle/Isar languages).
In this paper we give an algorithm for converting tree style proofs to flag style proofs. We then present a rewrite system that simplifies the results.
This algorithm can be used to convert arbitrary procedural proofs to declarative proofs. It does not work on the level of the proof terms (the basic inferences of the system), but on the level of the statements that the user sees in the goals when constructing the proof.
The algorithm from this paper has been implemented in the ProofWeb interface to Coq. In ProofWeb a proof that is given as a Coq proof script (even with arbitrary Coq tactics) can be displayed both as a tree style and as a flag style proof.
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.
References
Asperti, A., Padovani, L., Sacerdoti Coen, C., Guidi, F., Schena, I.: Mathematical Knowledge Management in HELM. Annals of Mathematics and Artificial Intelligence, Special Issue on Mathematical Knowledge Management 38, 1–3 (2003)
Asperti, A., Wegner, B.: MOWGLI – A New Approach for the Content Description in Digital Documents. In: Proceedings of the Nineth International Conference on Electronic Resources and the Social Role of Libraries in the Future, vol. 1 (2002)
Geuvers, H., Loeb, I.: From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions. In: Královič, R., Urzyczyn, P. (eds.) MFCS 2006. LNCS, vol. 4162, pp. 39–57. Springer, Heidelberg (2006)
Geuvers, H., Nederpelt, R.: Rewriting for Fitch Style Natural Deductions. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 134–154. Springer, Heidelberg (2004)
Girard, J.Y.: Linear Logic. Theor. Comput. Sci. 50, 1–102 (1987)
Guilhot, F., Naciri, H., Pottier, L.: Proof explanations: using natural language and graph view, Slides for a talk at a MoWGLI presentation (2003)
Harrison, J.R.: Proof Style. In: Giménez, E., Paulin-Möhring, C. (eds.) TYPES 1996. LNCS, vol. 1512, pp. 154–172. Springer, Heidelberg (1996)
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd edn. Cambridge University Press, Cambridge (2004)
Kaliszyk, C., van Raamsdonk, F., Wiedijk, F., Wupper, H., Hendriks, M., de Vrijer, R.: Deduction using the ProofWeb system. Technical Report ICIS–R08016, Radboud University Nijmegen (September 2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kaliszyk, C., Wiedijk, F. (2009). Merging Procedural and Declarative Proof. In: Berardi, S., Damiani, F., de’Liguoro, U. (eds) Types for Proofs and Programs. TYPES 2008. Lecture Notes in Computer Science, vol 5497. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02444-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-02444-3_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02443-6
Online ISBN: 978-3-642-02444-3
eBook Packages: Computer ScienceComputer Science (R0)