Abstract
Some general reflections on proof transformations lead to the abstract concept of a quintessential proof of a theorem. A quintessential proof embodies the essential features of many intertranslatable proofs of the theorem. While reasonable candidates for quintessential proofs for normal proofs have been developed, more work is needed with regard to non-normal proofs. Work on proof transformations seems likely to lead to important progress in understanding proofs.
This material is based upon work supported by the National Science Foundation under grants CCR-9732312 and CCR-0097179. It is based on a lecture which was given June 19, 2001 to the Workshop on Proof Transformations, Proof Presentations and Complexity of Proofs which was held in conjunction with IJCAR-2001 (International Joint Conference on Automated Reasoning) in Siena, Italy.
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
Andrews, P.B.: Resolution in Type Theory. Journal of Symbolic Logic 36, 414–432 (1971)
Andrews, P.B.: Transforming Matings into Natural Deduction Proofs. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, pp. 281–292. Springer, Heidelberg (1980)
Andrews, P.B.: Theorem Proving via General Matings. Journal of the ACM 28, 193–214 (1981)
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, London (1986)
Andrews, P.B., Bishop, M., Brown, C.E.: System Description: TPS: A Theorem Proving System for Type Theory. In: Mcallester [44], pp. 164–169
Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: A Theorem Proving System for Classical Type Theory. Journal of Automated Reasoning 16, 321–353 (1996)
Andrews, P.B., Miller, D.A., Cohen, E.L., Pfenning, F.: Automating Higher-Order Logic. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automated Theorem Proving: After 25 Years. Contemporary Mathematics series, vol. 29, pp. 169–192. American Mathematical Society, Providence (1984)
Barwise, J., Etchemendy, J.: Visual Information and Valid Reasoning. In: Zimmermann, W., Cunningham, S. (eds.) Visualization in Teaching and Learning Mathematics, pp. 9–24. Mathematical Association of America (1991)
Chester, D.: The Translation of Formal Proofs into English. Artificial Intelligence 7, 261–278 (1976)
Church, A.: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5, 56–68 (1940)
Coscoy, Y., Kahn, G., Théry, L.: Extracting Text from Proofs. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 109–123. Springer, Heidelberg (1995)
Courant, R., Robbins, H.: What is Mathematics? Oxford University Press, Oxford (1941)
Dahn, B.I., Gehne, J., Honigmann, T., Wolf, A.: Integration of Automated and Interactive Theorem Proving in ILF. In: McCune [45], pp. 57–60
Dahn, B.I., Wolf, A.: A Calculus Supporting Structured Proofs. Journal for Information Processing and Cybernetics (EIK) 30, 261–276 (1994)
Dahn, B.I., Wolf, A.: Natural Language Representation and Combination of Automatically Generated Proofs. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Munich (Germany). Applied Logic, pp. 175–192. Kluwer Academic Publishers, Dordrecht (1996)
Edgar, A., Pelletier, F.J.: Natural Language Explanations of Natural Deduction Proofs. In: Proceedings of the First Pacific Rim Conference on Computational Linguistics, Vancouver, pp. 269–278 (1993)
Egli, U., Schmitt, S.: Intuitionistic Proof Transformations and Their Application to Constructive Program Synthesis. In: Calmet, J., Plaza, J. (eds.) AISC 1998. LNCS (LNAI), vol. 1476, pp. 132–144. Springer, Heidelberg (1998)
Egly, U., Schmitt, S.: On Intuitionistic Proof Transformations, their Complexity, and Application to Constructive Program Synthesis. Fundamenta Informaticae 39, 59–83 (1999)
Fehrer, D., Horacek, H.: Exploiting the Addressee’s Inferential Capabilities in Presenting Mathematical Proofs. In: Pollack [54], pp. 959–964
Fiedler, A.: Using a Cognitive Architecture to Plan Dialogs for the Adaptive Explanation of Proofs. In: Dean, T. (ed.) Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI), Stockholm, SWEDEN, pp. 358–363. Morgan Kaufmann, San Francisco (1999)
Fiedler, A.: Dialog-driven Adaptation of Explanations of Proofs. In: Nebel, B. (ed.) Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI), Seattle, WA, pp. 1295–1300. Morgan Kaufmann, San Francisco (2001)
Fiedler, A.: P.rex: An Interactive Proof Explainer. In: Goré, et al. [26], pp. 416–420
Fiedler, A.: User-Adaptive Proof Explanation. PhD thesis, Naturwissenschaftlich- Technische Fakultät I, Universität des Saarlandes, Saarbrücken, Germany (2001)
Gentzen, G.: Untersuchungen über das Logische Schließen I und II. Mathematische Zeitschrift 39, 176–210, 405–431 (1935); Translated in [25]
Gentzen, G.: Investigations into Logical Deductions. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland Publishing Co., Amsterdam (1969)
Goré, R., Leitsch, A., Nipkow, T. (eds.): IJCAR 2001. LNCS (LNAI), vol. 2083. Springer, Heidelberg (2001)
Hammer, E.M.: Logic and Visual Information. CSLI Publications & FoLLI, Stanford (1995)
Herbrand, J.: Recherches sur la théorie de la démonstration. Travaux de la Société des Sciences et des Lettres de Varsovie, Classe III Sciences Mathematiques et Physiques 33 (1930); Translated in [29]
Herbrand, J.: Logical Writings. Harvard University Press (1971) Edited by Warren D. Goldfarb
Holland-Minkley, A.M., Barzilay, R., Constable, R.L.: Verbalization of High-Level Formal Proofs. In: Proceedings of the Sixteenth National Conference on Artificial Intelligence (AAAI 1999) and Eleventh Innovative Application of Artificial Intelligence Conference (IAAI 1999), pp. 277–284. AAAI Press, Menlo Park (1999)
Horacek, H.: A Model for Adapting Explanations to the User’s Likely Inferences. User Modeling and User-Adapted Interaction 7, 1–55 (1997)
Horacek, H.: Presenting Proofs in a Human-Oriented Way. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 142–156. Springer, Heidelberg (1999)
Huang, X.: Proof Transformation Towards Human Reasoning Style. In: Metzing, D. (ed.) Proceedings of the 13th German Workshop on Artificial Intelligence, Informatik-Fachberichte, vol. 216, pp. 37–42. Springer, Heidelberg (1989)
Huang, X.: Reference Choices in Mathematical Proofs. In: Aiello, L.C. (ed.) Proceedings of the 9th European Conference on Artificial Intelligence, pp. 720–725. Pitman Publishing (1990)
Huang, X.: Human Oriented Proof Presentation: A Reconstructive Approach. PhD thesis, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany (1994)
Huang, X.: Proverb: A System Explaining Machine-Found Proofs. In: Ram, A., Eiselt, K. (eds.) Proceedings of Sixteenth Annual Conference of the Cognitive Science Society, Atlanta, USA, pp. 427–432. Lawrence Erlbaum Associates, Mahwah (1994)
Huang, X.: Reconstructing Proofs at the Assertion Level. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 738–752. Springer, Heidelberg (1994)
Huang, X.: Translating Machine-Generated Resolution Proofs into NDProofs at the Assertion Level. In: Foo, N.Y., Göbel, R. (eds.) PRICAI 1996. LNCS (LNAI), vol. 1114, pp. 399–410. Springer, Heidelberg (1996)
Huang, X., Fiedler, A.: Presenting Machine-Found Proofs. In: McRobbie, Slaney [46], pp. 221–225
Huang, X., Fiedler, A.: Proof Verbalization as an Application of NLG. In: Pollack [54], pp. 965–971
Kreitz, C., Schmitt, S.: A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems. Information and Computation 162(1-2), 226–254 (2000)
Lingenfelder, C.: Structuring Computer Generated Proofs. In: Sridharan, N.S. (ed.) Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, IJCAI, Detroit, Michigan, USA, pp. 378–383. Morgan Kaufmann, San Francisco (1989)
Lingenfelder, C.: Transformation and Structuring of Computer Generated Proofs. PhD thesis, University of Kaiserslautern, 115 p. (1990)
Mcallester, D. (ed.): CADE 2000. LNCS (LNAI), vol. 1831. Springer, Heidelberg (2000)
McCune, W. (ed.): CADE 1997. LNCS (LNAI), vol. 1249. Springer, Heidelberg (1997)
McRobbie, M.A., Slaney, J.K. (eds.): CADE 1996. LNCS (LNAI), vol. 1104. Springer, Heidelberg (1996)
Meier, A.: System Description: Tramp: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level. In: Mcallester [44], pp. 460–464
Miller, D.A.: Proofs in Higher-Order Logic. PhD thesis, Carnegie Mellon University, 81 p. (1983)
Miller, D.A.: Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. In: Shostak (ed.) [61], pp. 375–393
Miller, D.A.: A Compact Representation of Proofs. Studia Logica 46(4), 347–370 (1987)
Pfenning, F.: Analytic and Non-Analytic Proofs. In: Shostak [61], pp. 394–413
Pfenning, F.: Proof Transformations in Higher-Order Logic. PhD thesis, Carnegie Mellon University, 156 p. (1987)
Pierce, W.: Toward Mechanical Methods for Streamlining Proofs. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol. 449, pp. 351–365. Springer, Heidelberg (1990)
Pollack, M.E. (ed.): Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), Nagoya, JAPAN. Morgan Kaufmann, San Francisco (1997)
Schmitt, S.: A Tableau-Like Representation Framework for Efficient Proof Reconstruction. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS (LNAI), vol. 1847, pp. 398–414. Springer, Heidelberg (2000)
Schmitt, S., Kreitz, C.: On Transforming Intuitionistic Matrix Proofs into Standard-Sequent Proofs. In: Baumgartner, P., Posegga, J., Hähnle, R. (eds.) TABLEAUX 1995. LNCS (LNAI), vol. 918, pp. 106–121. Springer, Heidelberg (1995)
Schmitt, S., Kreitz, C.: Converting Non-Classical Matrix proofs into Sequent-Style Systems. In: McRobbie, Slaney [46], pp. 418–432
Schmitt, S., Kreitz, C.: Deleting Redundancy in Proof Reconstruction. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 262–276. Springer, Heidelberg (1998)
Schmitt, S., Lorigo, L., Kreitz, C., Nogin, A.: JProver: Integrating Connection-based Theorem Proving into Interactive Proof Assistants. In: Goré, et al. [26], pp. 421–426
Shin, S.-J.: The Logical Status of Diagrams. Cambridge University Press, Cambridge (1994)
Shostak, R.E. (ed.): CADE 1984. LNCS, vol. 170. Springer, Heidelberg (1984)
Wolf, A.: Optimization and Translation of Tableau-Proofs into Resolution. Journal of Information Processing and Cybernetics (EIK) 30(5-6), 311–325 (1994)
Wolf, A.: A Translation of Model Elimination Proofs into a Structured Natural Deduction. In: Dankel II, D.D. (ed.) Proc. of 10th Int. Florida AI Research Society Conference, Daytona Beach, FL, USA, pp. 11–15. Florida AI Research Society (1997)
Wolf, A.: A Step Towards a Better Understanding of Automatically Generated Model Elimination Proofs. In: Cuena, J. (ed.) Information Technologies and Knowledge Systems (IT&KNOWS 1998) – Proceedings of the XV. IFIP World Computer Congress. Österreichische Computergesellschaft/ International Federation for Information Processing, pp. 415–428 (1998)
Wolf, A., Schumann, J.: ILF-SETHEO: Processing Model Elimination Proof for Natural Language Output. In: McCune [45], pp. 61–64
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Andrews, P.B. (2005). Some Reflections on Proof Transformations. In: Hutter, D., Stephan, W. (eds) Mechanizing Mathematical Reasoning. Lecture Notes in Computer Science(), vol 2605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32254-2_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-32254-2_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25051-7
Online ISBN: 978-3-540-32254-2
eBook Packages: Computer ScienceComputer Science (R0)