Can Proofs be Animated by Games?

• Autorzy: Hayashi S.
• Języki publikacji: EN

Abstrakty

EN

Proof animation is a way of executing proofs to find errors in the formalization of proofs. It is intended to be "testing in proof engineering". Although the realizability interpretation as well as the functional interpretation based on limit-computations were introduced as means for proof animation, they were unrealistic as an architectural basis for actual proof animation tools. We have found a game theoretic semantics corresponding to these interpretations, which is likely to be the right architectural basis for proof animation.

Słowa kluczowe

EN

game semantics; computations in classical logic; learning theory

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 77, nr 4
• Strony: 331--343
• Opis fizyczny: bibliogr. 20 poz.

Twórcy

autor

Hayashi S.

• Prof. Susumu Hayashi, Humanistic Informatics, Graduate School of Letters, Kyoto University, Yoshida-Honmachi, Sakyo, Kyoto, 606-8501, Japan,

Bibliografia

• [1] Akama, Y., Berardi, S., Hayashi, S. and Kohlenbach, U.: An arithmetical hierarchy of the law of excluded middle and related principles, in Proceedings of 19th IEEE Symposium on Logic in Computer Science, Turku, Finland, 2004, 192-201.
• [2] Berardi, S.: Classical logic as limit completion. Mathematical Structures in Computer Science 15(1), 2005, 167-200.
• [3] Berardi, S., Coquand, T. and Hayashi, S.: Games with 1-Backtracking, in Proceedings of GALOP 2005, 210-225.
• [4] Coquand, T.: A Semantics of Evidence for Classical Arithmetic, in Géard Huet, Gordon Plotkin and Claire Jones, eds, Proceedings of the SecondWorkshop on Logical Frameworks, 1991, (a preliminary version of [5]).
• [5] Coquand, T.: A Semantics of Evidence for Classical Arithmetic, Journal of Symbolic Logic 60(1), 1995, 325-337.
• [6] Hayashi, S. and Nakano, H.: PX: A Computational Logic, 1988, The MIT Press, available free from the author's web page in PDF format.
• [7] Hayashi, S. and Nakata, M.: Towards Limit Computable Mathematics, in the Proceedings of Types for Proofs and Programs, P. Challanghan, Z. Luo, J. McKinna, R. Pollack, eds., LNCS 2277, 2001, 125-144.
• [8] Hayashi, S., Sumitomo, R. and Shii, K.: Towards Animation of Proofs - Testing Proofs by Examples -, Theoretical Computer Science 272(1-2), 2002, 177-195.
• [9] Hayashi, S.: Mathematics based on Incremental Learning, -Excluded middle and Inductive inference-, Theoretical Computer Science 350(1), 2005, 125-139.
• [10] Hilbert, D.: über die Theorie der algebraische Formen, Mathematische Annalen 36, 1890, 473-531.
• [11] Hilbert, D.: Theory of Algebraic Invariants, translated by Laubenbacher, R.L., Cambridge University Press, 1993.
• [12] Hintikka, J. and Kulas, J.: The Game of Language, Reidel, 1983.
• [13] Hintikka, J. and Sandu, G.: Game-Theoretical Semantics, in Handbook of Logic and Language, Part I, edited by van Benthem Jan F. A. K. et al., 1997, Elsevier, 361-410.
• [14] Jackson, M.: Software Specifications and Requirements: a lexicon of practice, principles and prejudices, Addison-Wesley, 1995.
• [15] Kohlenbach, U. and Oliva, P.: Proof mining: a systematic way of analysing proofs in Mathematics, in Proceedings of the Steklov Institute of Mathematics 242, 136-164, 2003.
• [16] Nakata,M. and Hayashi, S.: Realizability Interpretation for Limit ComputableMathematics, ScientiaeMathematicae Japonicae 5, 421-434, 2001.
• [17] Odifreddi, P.G.: Classical Recursion Theory, North-Holland, 1992.
• [18] Sommerville, I.: Software engineering, 7th edition, AddisonWesley, 2004.
• [19] Sanjay, J., Osherson, D., Royer, J.S., and Sharma, A.: Systems That Learn - 2nd Edition: An Introduction to Learning Theory Learning, Development, and Conceptual Change, The MIT Press, 1999.
• [20] Toftdal, M.: A Calibration of Ineffective Theorems of Analysis in a Hierarchy of Semi-Classical Logical Principles, in Proceedings of ICALP '04, 2004, 1188-1200.