{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:04:53Z","timestamp":1776553493011,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540671909","type":"print"},{"value":"9783540465089","type":"electronic"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46508-1_9","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:02:03Z","timestamp":1186156923000},"page":"137-151","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Interpretation of a Mizar-Like Logic in First Order Logic"],"prefix":"10.1007","author":[{"given":"Ingo","family":"Dahn","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/0003-4843(74)90016-3","volume":"7","author":"K. J. Barwise","year":"1974","unstructured":"K. J. Barwise: Axioms for abstract model theory; Ann. Math. Logic vol. 7 (1974), 221\u2013265","journal-title":"Ann. Math. Logic"},{"key":"9_CR2","unstructured":"I. Dahn, C. Wernhard: First Order Proof Problems Extracted from an Article in the MIZAR Mathematical Library. RISC-Linz Report Series, No. 97-50, pp. 58\u201362, Johannes Kepler Universit\u00e4t Linz, 1997."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"B. I. Dahn, J. Gehne, Th. Honigmann, A. Wolf: Integration of Automated and Interactive Theorem Proving in Ilf. In Proc. CADE-14, pp. 57\u201360, Springer, 1997.","DOI":"10.1007\/3-540-63104-6_7"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"H. Ganzinger, C. Meyer, C. Weidenbach: Soft Typing for Ordered Resolution. In Proc. CADE-14, pp. 321\u2013335, Springer, 1997.","DOI":"10.1007\/3-540-63104-6_32"},{"key":"9_CR5","first-page":"40","volume":"14","author":"C. S. Mellish","year":"1988","unstructured":"Mellish, C. S.: Implementing Systemic Classification by Unification. Comp. Ling. 14, 1988, pp 40\u201351","journal-title":"Comp. Ling."},{"key":"9_CR6","unstructured":"The Mizar Library Committee: Syntax of the Mizar Language. \n                    http:\/\/www.mizar.org\/language\/syntax.txt"},{"key":"9_CR7","volume-title":"Proceedings of the 1992 Workshop on Types for Proofs and Programs","author":"P. Rudnicki","year":"1992","unstructured":"P. Rudnicki: An Overview of the Mizar Project. Proceedings of the 1992 Workshop on Types for Proofs and Programs, Chalmers University of Technology, Bastad 1992."},{"key":"9_CR8","doi-asserted-by":"crossref","first-page":"68","DOI":"10.4064\/fm-30-1-68-89","volume":"30","author":"A. Tarski","year":"1938","unstructured":"A. Tarski \u201cUber unerreichbare Kardinalzahlen, Fund. Math., vol.30 (1938), pp.68\u201369","journal-title":"Fund. Math."},{"key":"9_CR9","unstructured":"A. Trybulec: Some Features of the Mizar Language, ESPRIT Workshop, Torino 1993."},{"key":"9_CR10","unstructured":"G. Wiederhold, M. Genesereth: The Basis for Mediation. To appear IEEE Expert"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Classical and Non-Classical Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46508-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T09:50:06Z","timestamp":1558259406000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"17 May 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}