{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T19:31:46Z","timestamp":1694633506073},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2008,6,6]],"date-time":"2008-06-06T00:00:00Z","timestamp":1212710400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Intell Inf Syst"],"published-print":{"date-parts":[[2008,10]]},"DOI":"10.1007\/s10844-008-0059-2","type":"journal-article","created":{"date-parts":[[2008,6,5]],"date-time":"2008-06-05T03:45:19Z","timestamp":1212637519000},"page":"111-125","source":"Crossref","is-referenced-by-count":1,"title":["A framework for checking proofs naturally"],"prefix":"10.1007","volume":"31","author":[{"given":"Masahiko","family":"Sato","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,6,6]]},"reference":[{"key":"59_CR1","volume-title":"Automated deduction (Vol. 2)","author":"H. Benl","year":"1998","unstructured":"Benl, H., Berger, U., Seisenberger, M., Schwichtenberg, H., & Zuber, W. (1998). Proof theory at work: Program development in the Minlog system. In W. Bibel & P.H. Schmitt (Eds.), Automated deduction (Vol. 2). Deventer: Kluwer."},{"key":"59_CR2","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/S0019-9958(82)90458-2","volume":"55","author":"K. J. Berkling","year":"1982","unstructured":"Berkling, K. J., & Fehr, E. (1982). A consistent extension of the lambda calculus as a base for functional programming languages. Information and Control, 55, 89\u2013101.","journal-title":"Information and Control"},{"key":"59_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive theorem proving and program development, coq\u2019art: The calculus of inductive constructions. Texts in theoretical computer science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., & Cast\u00e9ran, P. (2004). Interactive theorem proving and program development, coq\u2019art: The calculus of inductive constructions. Texts in theoretical computer science. Berlin: Springer."},{"key":"59_CR4","first-page":"98","volume-title":"Symbolic computation and automated reasoning (Proceedings of CALCULEMUS 2000, Symposium on the integration of symbolic computation and mechanized reasoning, St. Andrews, Scotland, August 6\u20137)","author":"B. Buchberger","year":"2000","unstructured":"Buchberger, B., Dupre, C., Jebelean, T., Kriftner, F., Nakagawa, K., Vasaru, D., et al. (2000). The theorema project: A progress report. In M. Kerber & M. Kohlhase (Eds.), Symbolic computation and automated reasoning (Proceedings of CALCULEMUS 2000, Symposium on the integration of symbolic computation and mechanized reasoning, St. Andrews, Scotland, August 6\u20137) (pp. 98\u2013113). Massachusetts: AK Peters, Natick."},{"key":"59_CR5","doi-asserted-by":"crossref","DOI":"10.1525\/9780520312364","volume-title":"The basic laws of arithmetic","author":"G. Frege","year":"1964","unstructured":"Frege, G. (1964). The basic laws of arithmetic. Berkeley: University of California Press."},{"key":"59_CR6","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., & Plotkin, G. (1993). A framework for defining logic. Journal of the Association for Computing Machinery, 40, 143\u2013184.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"59_CR7","volume-title":"Selected papers on automath. Studies in logic and the foundations of mathematics (Vol. 133)","year":"1994","unstructured":"Nederpelt, R. P., Geuvers, J. H., & de Vrijer, R. C. (Eds.) (1994). Selected papers on automath. Studies in logic and the foundations of mathematics (Vol. 133). Amsterdam: North-Holland."},{"key":"59_CR8","volume-title":"Isabelle\/HOL \u2014 A proof assistant for higher-order logic, lecture notes in computer science (Vol. 2283)","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L. C., & Wenzel, M. (2002). Isabelle\/HOL \u2014 A proof assistant for higher-order logic, lecture notes in computer science (Vol. 2283). Berlin: Springer."},{"key":"59_CR9","volume-title":"Programming in Martin-L\u00f6f\u2019s type theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., & Smith, J. M. (1990). Programming in Martin-L\u00f6f\u2019s type theory. Oxford: Clarendon."},{"key":"59_CR10","first-page":"61","volume":"5","author":"F. Pfenning","year":"2005","unstructured":"Pfenning, F., & Harper, R. (2005). On equivalence and canonical forms in the LF type theory. Transactions on Computational Logic, 5, 61\u2013101.","journal-title":"Transactions on Computational Logic"},{"key":"59_CR11","first-page":"202","volume-title":"Proceedings of the 16th international conference on automated deduction (CADE-16). Lecture notes in artificial intelligence (Vol. 1632","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., & Sch\u00fcrmann, C. (1999). Twelf \u2013 a meta-logical framework for deductive systems. In H. Ganzinger (Ed.), Proceedings of the 16th international conference on automated deduction (CADE-16). Lecture notes in artificial intelligence (Vol. 1632, pp. 202\u2013206). Berlin: Springer.","edition":"1632"},{"key":"59_CR12","doi-asserted-by":"crossref","DOI":"10.4159\/9780674042469","volume-title":"Mathematical logic, (revised ed.)","author":"W. V. O. Quine","year":"1951","unstructured":"Quine, W. V. O. (1951). Mathematical logic, (revised ed.). Cambridge: Harvard University Press."},{"key":"59_CR13","doi-asserted-by":"crossref","unstructured":"Sato, M. (1985). Theory of symbolic expressions II. Publications of the Research Institute for Mathematical Sciences, Kyoto University, 21, 455\u2013540.","DOI":"10.2977\/prims\/1195179055"},{"key":"59_CR14","first-page":"78","volume-title":"Progress in discovery science. Lecture notes in artificial intelligence (Vol. 2281","author":"M. Sato","year":"2002","unstructured":"Sato, M. (2002). Theory of judgments and derivations. In S. Arikawa & A. Shinohara (Eds.), Progress in discovery science. Lecture notes in artificial intelligence (Vol. 2281, pp. 78\u2013122). Berlin: Springer."},{"key":"59_CR15","first-page":"437","volume-title":"ASIAN 2004. Lecture notes in computer science (Vol. 3321)","author":"M. Sato","year":"2004","unstructured":"Sato, M. (2004). A simple theory of expressions, judgments and derivations. In M. J. Maher (Ed.), ASIAN 2004. Lecture notes in computer science (Vol. 3321, pp. 437\u2013451). Berlin: Springer."},{"key":"59_CR16","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1007\/3-540-45654-6_40","volume-title":"Computer aided systems theory \u2013 EUROCAST 2001. Lecture notes in computer science (Vol. 2718)","author":"M. Sato","year":"2001","unstructured":"Sato, M., Kameyama, Y., & Takeuti, I. (2001). CAL: A computer assisted learning system for computation and logic. In R. Moreno-Diaz, B. Buchberger, & J-L. Freire (Eds.), Computer aided systems theory \u2013 EUROCAST 2001. Lecture notes in computer science (Vol. 2718, pp. 509\u2013524). Berlin: Springer."}],"container-title":["Journal of Intelligent Information Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10844-008-0059-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10844-008-0059-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10844-008-0059-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,11]],"date-time":"2021-09-11T17:55:26Z","timestamp":1631382926000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10844-008-0059-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,6,6]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,10]]}},"alternative-id":["59"],"URL":"https:\/\/doi.org\/10.1007\/s10844-008-0059-2","relation":{},"ISSN":["0925-9902","1573-7675"],"issn-type":[{"value":"0925-9902","type":"print"},{"value":"1573-7675","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,6,6]]}}}