{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:10:18Z","timestamp":1725455418915},"publisher-location":"Berlin\/Heidelberg","reference-count":14,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540167838"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0016237","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T05:39:17Z","timestamp":1131860357000},"page":"113-127","source":"Crossref","is-referenced-by-count":1,"title":["An approach to proof checker"],"prefix":"10.1007","author":[{"given":"Ken","family":"Hirose","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"T. Ida, M.Sato, S.Hayashi, M.Hagiya et al, \u201cHigher Order: its Implication to Programming Languages and Computational Models\u201d, ICOT TM-29, 1983."},{"key":"8_CR2","unstructured":"ICOT Working Group 5, \u201cSeveral Aspects on Unification\u201d, ICOT TM-46, 1984."},{"key":"8_CR3","unstructured":"M. Sato, \u201cTyped Logical Calculus\u201d, TR-85-13, Dept. of Computer Science,Fac. of Science, Univ. of Tokyo, 1985."},{"key":"8_CR4","unstructured":"M.Sato and T.Sakurai, \u201cQute: A Functional Language based on Unification\u201d, Proceedings of the International Conference on Fifth Generation Computer Systems, pp157\u2013165, 1984."},{"key":"8_CR5","unstructured":"A.Kock, Synthetic Differential Geometry, London Mathematical Society Lecture Note Series 51, Cambridge University Press, pp311, 1981."},{"key":"8_CR6","unstructured":"S.Hayashi, \u201cTowards Automated Synthetic Differential Geometry 1 \u2014 basic categorical construction\u201d, ICOT TR-104, 1985."},{"key":"8_CR7","unstructured":"S.Uchida and T.Yokoi, \u201cSequential Inference Machine: SIM Progress Report\u201d, ICOT TR-86, 1984."},{"key":"8_CR8","unstructured":"T.Yokoi and S.Uchida, \u201cSequential Inference Machine: SIM Its Programming and Operating System\u201d, ICOT TR-87, 1984."},{"key":"8_CR9","unstructured":"T.Chikayama, \u201cUnique Feature of ESP\u201d, Proceedings of the International Conference of the Fifth Generation Computer System, Tokyo, pp292\u2013298, 1984."},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"M.J.Gorden, A.J.Milner and C.P.Wadsworth, \u201cEdinburgh LCF\u201d, Lecture Notes in Computer Science,78, Springer, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"8_CR11","unstructured":"J. Ketonen and J.S. Weening, \u201cEKL \u2014 An Interactive Proof Checker, User's Reference Manual\u201d, Department of Computer Science, Stanford Univ., 1983."},{"key":"8_CR12","unstructured":"M.Hagiya and S.Hayashi, \u201cSome Experiments on EKL\u201d, ICOT TM-101, 1985."},{"key":"8_CR13","first-page":"26","volume":"85","author":"A. Tryburec","year":"1985","unstructured":"A. Tryburec and H. Blair, \u201cComputer Assisted Reasoning with Mizar\u201d, I JCAI' 85, pp26\u201328, 1985.","journal-title":"I JCAI'"},{"key":"8_CR14","first-page":"407","volume":"1","author":"N. Shanker","year":"1985","unstructured":"N. Shanker, \u201cTowards Mechanical Metamathematics\u201d, Journal of Automated Reasoning, 1, pp407\u2013434, 1985.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 1986"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0016237.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:35:31Z","timestamp":1607549731000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0016237"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540167838"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0016237","relation":{},"subject":[]}}