{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:27:09Z","timestamp":1725571629358},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255932"},{"type":"electronic","value":"9783540320142"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11417170_3","type":"book-chapter","created":{"date-parts":[[2010,12,16]],"date-time":"2010-12-16T19:29:35Z","timestamp":1292527775000},"page":"11-22","source":"Crossref","is-referenced-by-count":2,"title":["Can Proofs Be Animated By Games?"],"prefix":"10.1007","author":[{"given":"Susumu","family":"Hayashi","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Akama, Y., Berardi, S., Hayashi, S., Kohlenbach, U.: An arithmetical hierarchy of the law of excluded middle and related principles."},{"key":"3_CR2","unstructured":"Berardi, S.: Classical logic as Limit Completion. In: A constructive model for non-recursive maps (2001) (submitted), available at http:\/\/www.di.unito.it\/~stefano\/"},{"key":"3_CR3","unstructured":"Berardi, S., Coquand, T., Hayashi, S.: Games with 1-Backtracking (2005) (submitted)"},{"key":"3_CR4","unstructured":"Coquand, T.: A Semantics of Evidence for Classical Arithmetic. In: G\u00e9ard Huet, G., Plotkin, C., Jones (eds.) Proceedings of the Second Workshop on Logical Frameworks (1991) (a preliminary version of [5])"},{"issue":"1","key":"3_CR5","doi-asserted-by":"publisher","first-page":"325","DOI":"10.2307\/2275524","volume":"60","author":"T. Coquand","year":"1995","unstructured":"Coquand, T.: A Semantics of Evidence for Classical Arithmetic. Journal of Symbolic Logic\u00a060(1), 325\u2013337 (1995)","journal-title":"Journal of Symbolic Logic"},{"key":"3_CR6","unstructured":"Hayashi, S., Nakano, H.: PX: A Computational Logic. The MIT Press, Cambridge (1988); available free from the author\u2019s web page in PDF format."},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Hayashi, S., Nakata, M.: Towards Limit Computable Mathematics, in Types for Proofs and Programs. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 125\u2013144. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45842-5_9"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0304-3975(00)00350-9","volume":"272","author":"S. Hayashi","year":"2002","unstructured":"Hayashi, S., Sumitomo, R., Shii, K.: Towards Animation of Proofs - Testing Proofs by Examples. Theoretical Computer Science\u00a0272, 177\u2013195 (2002)","journal-title":"Theoretical Computer Science"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Hayashi, S.: Mathematics based on Incremental Learning, -Excluded middle and Inductive inference. Theoretical Computer Science (to appear)","DOI":"10.1016\/j.tcs.2005.10.019"},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/BF01208503","volume":"36","author":"D. Hilbert","year":"1890","unstructured":"Hilbert, D.: \u00dcber die Theorie der algebraische Formen. Mathematische Annalen\u00a036, 473\u2013531 (1890)","journal-title":"Mathematische Annalen"},{"key":"3_CR11","volume-title":"Theory of Algebraic Invariants, translated by Laubenbacher, R.L.","author":"D. Hilbert","year":"1993","unstructured":"Hilbert, D.: Theory of Algebraic Invariants, translated by Laubenbacher, R.L. Cambridge University Press, Cambridge (1993)"},{"key":"3_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-010-9847-2","volume-title":"The Game of Language","author":"J. Hintikka","year":"1983","unstructured":"Hintikka, J., Kulas, J.: The Game of Language. Reidel, Dordrechtz (1983)"},{"key":"3_CR13","unstructured":"Hintikka, J., Sandu, G.: Game-Theoretical Semantics. In: van Benthem Jan, F.A.K., et al. (eds.) Handbook of Logic and Language, Part I (1999)"},{"key":"3_CR14","unstructured":"Kohlenbach, U., Oliva, P.: Proof mining: a systematic way of analysing proofs in Mathematics. In: Proceedings of the Steklov Institute of Mathematics, vol.242, pp. 136\u2013164 (2003)"},{"key":"3_CR15","first-page":"421","volume":"5","author":"M. Nakata","year":"2001","unstructured":"Nakata, M., Hayashi, S.: Realizability Interpretation for Limit Computable Mathematics. Scientiae Mathematicae Japonicae\u00a05, 421\u2013434 (2001)","journal-title":"Scientiae Mathematicae Japonicae"},{"key":"3_CR16","volume-title":"Software engineering","author":"I. Sommerville","year":"2000","unstructured":"Sommerville, I.: Software engineering, 6th edn. Addison Wesley, Reading (2000)","edition":"6"},{"key":"3_CR17","volume-title":"Systems That Learn - 2nd Edition: An Introduction to Learning Theory (Learning, Development, and Conceptual Change)","author":"J. Sanjay","year":"1999","unstructured":"Sanjay, J., Osherson, D., Royer, J.S., Sharma, A.: Systems That Learn - 2nd Edition: An Introduction to Learning Theory (Learning, Development, and Conceptual Change). The MIT Press, Cambridge (1999)"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1188","DOI":"10.1007\/978-3-540-27836-8_98","volume-title":"Automata, Languages and Programming","author":"M. Toftdal","year":"2004","unstructured":"Toftdal, M.: A Calibration of Ineffective Theorems of Analysis in a Hierarchy of Semi-Classical Logical Principles. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 1188\u20131200. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11417170_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:51:56Z","timestamp":1605642716000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11417170_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255932","9783540320142"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/11417170_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}