{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:04:51Z","timestamp":1776553491306,"version":"3.51.2"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2004,10,1]],"date-time":"2004-10-01T00:00:00Z","timestamp":1096588800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2004,10]]},"DOI":"10.1007\/s10817-004-6245-1","type":"journal-article","created":{"date-parts":[[2005,3,8]],"date-time":"2005-03-08T14:23:45Z","timestamp":1110291825000},"page":"319-339","source":"Crossref","is-referenced-by-count":33,"title":["MPTP ? Motivation, Implementation, First Experiments"],"prefix":"10.1007","volume":"33","author":[{"given":"Josef","family":"Urban","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,2,28]]},"reference":[{"key":"CR1","first-page":"65","volume-title":"Symbolic Computation and Automated Reasoning","author":"G. Bancerek","year":"2000","unstructured":"Bancerek, G. (2000) Development of the theory of continuous lattices in Mizar, in M. Kerber and M. Kohlhase (eds.), Symbolic Computation and Automated Reasoning, The CALCULEMUS-2000 Symposium, A. K. Peters, Natick, MA, pp. 65?80."},{"key":"CR2","unstructured":"Carlson, A. J., Cumby, C. M., Rosen, J. L. and Roth, D. (1999) SNoW user?s guide, UIUC Tech Report UIUC-DCS-R-99-210."},{"key":"CR3","unstructured":"Dahn, I. and Wernhard, C. (1997) First order proof problems extracted from an article in the MIZAR mathematical library, in Proceedings of the International Workshop on First Order Theorem Proving, RISC-Linz Report Series, No. 97-50, Johannes Kepler Universit\u00e4t Linz."},{"key":"CR4","unstructured":"Dahn, I. (1998) Interpretation of a Mizar-like logic in first order logic, in Proceedings of FTP 1998, pp. 137?151."},{"key":"CR5","unstructured":"Dahn, I. (2001) Slicing book technology ? Providing online support for textbooks, in Proc. ICDE 2001, International Conference on Distant Education, D\u00fcsseldorf."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Meyer, C. and Weidenbach, C. (1997) Soft typing for ordered resolution, in Proc. CADE-14, Springer, pp. 321?335.","DOI":"10.1007\/3-540-63104-6_32"},{"key":"CR7","unstructured":"Ganzinger, H. and Stuber, J. (2003) Superposition with equivalence reasoning and delayed clause normal form transformation, in Proc. 19th Int. Conf. on Automated Deduction (CADE-19), Miami, Florida, LNAI 2741, Springer, pp. 335?349."},{"key":"CR8","unstructured":"H\u00e4hnle, R., Kerber, M. and Weidenbach, C. (1996) Common syntax of the DFGSchwerpunktprogramm deduction, Technical Report TR 10\/96, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe, Karlsruhe, Germany."},{"key":"CR9","first-page":"251","volume-title":"Machine Intelligence 9","author":"D. B. Lenat","year":"1979","unstructured":"Lenat, D. B. (1979) On automated scientific theory formation: A case study using the AM program, in J. Hayes, D. Michie and L. I. Mikulich (eds.), Machine Intelligence 9, Halstead, New York, 1979, pp. 251?283."},{"issue":"2","key":"CR10","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0004-3702(82)90036-4","volume":"19","author":"D. B. Lenat","year":"1982","unstructured":"Lenat, D. B. (1982) The nature of heuristics, Artificial Intelligence 19(2) 189?249.","journal-title":"Artificial Intelligence"},{"issue":"3","key":"CR11","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. W. McCune","year":"1997","unstructured":"McCune, W. W. (1997) Solution of the Robbins problem, J. Automated Reasoning 19(3), 263?276.","journal-title":"J. Automated Reasoning"},{"key":"CR12","unstructured":"MoMM (2004) The MoMM interreduction system by Josef Urban, available online at http:\/\/alioth.uwb.edu.pl\/twiki\/bin\/view\/Mizar\/MoMM."},{"key":"CR13","unstructured":"MPTPResults.sql ? SQL structure of the MPTP result database, published online at http:\/\/alioth.uwb.edu.pl\/twiki\/bin\/view\/Mizar\/MpTP."},{"issue":"1","key":"CR14","first-page":"9","volume":"2","author":"A. Naumowicz","year":"2002","unstructured":"Naumowicz, A. and Byli?ski, C. (2002) Basic elements of computer algebra in MIZAR, Mechanized Mathematics and Its Applications 2(1), 9?16.","journal-title":"Mechanized Mathematics and Its Applications"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"Nonnengart, A. and Weidenbach, C. (2001) Computing small clause normal forms, in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Vol. 1, Elsevier, Chapter 6, pp. 335?367.","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"CR16","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1080\/11663081.1996.10510868","volume":"6","author":"J. L. Pollock","year":"1996","unstructured":"Pollock, J. L. (1996) OSCAR: A general purpose defeasible reasoner, J. Appl. Non-Classical Logics 6, 89?113.","journal-title":"J. Appl. Non-Classical Logics"},{"key":"CR17","volume-title":"Proceedings of the 1992 Workshop on Types for Proofs and Programs","author":"P. Rudnicki","year":"1992","unstructured":"Rudnicki, P. (1992) An overview of the Mizar project, in Proceedings of the 1992 Workshop on Types for Proofs and Programs, Chalmers University of Technology, Bastad."},{"key":"CR18","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S. (2002) E ? A brainiac theorem prover, J. AI Comm. 15, 111?126.","journal-title":"J. AI Comm."},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Schulz, S. (2001) Learning search control knowledge for equational theorem proving, in F. Baader, G. Brewka and T. Eiter (eds.), Proceedings of the Joint German\/Austrian Conference on Artificial Intelligence (KI-2001), LNAI 2174, Springer, pp. 320?334.","DOI":"10.1007\/3-540-45422-5_23"},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"Schumann, J. M. (2001) Automated Theorem-Proving in Software Engineering, Springer-Verlag.","DOI":"10.1007\/978-3-662-22646-9"},{"issue":"2","key":"CR21","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G. and Suttner, C. B. (1998) The TPTP problem library: CNF release v1.2.1, J. Automated Reasoning 21(2), 177?203.","journal-title":"J. Automated Reasoning"},{"key":"CR22","unstructured":"Sutcliffe, G., Zimmer, J. and Schulz, S. (2003) Communication formalisms for automated theorem proving tools, in V. Sorge, S. Colton, M. Fisher and J. Gow (eds.), Proceedings of the IJCAI-18 Workshop on Agents and Automated Reasoning, pp. 53?58."},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"Urban, J. (2003) Translating Mizar for first order theorem provers, in A. Asperti, B. Buchberger and J. Davenport (eds.), Mathematical Knowledge Management, Proceedings of MKM 2003, LNCS 2594.","DOI":"10.1007\/3-540-36469-2_16"},{"key":"CR24","unstructured":"Urban, J. (2004) MoMM ? Fast interreduction and retrieval in large libraries of formalized mathematics, in G. Sutcliffe, S. Schultz and T. Tammit (eds.), Proceedings of the IJCAR 2004 Workshop on Empirically Successful First Order Reasoning, ENTCS, accepted. Available online at http:\/\/ktiml.mff.cuni.cz\/~urban\/MoMM\/momm.ps"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"Weidenbach, C. (2001) SPASS: Combining superposition, sorts and splitting, in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Vol. II, Elsevier Science and MIT Press, Chapter 27, pp. 1965?2013.","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"key":"CR26","unstructured":"Wiedijk, F. (2000) CHECKER ? Notes on the basic inference step in Mizar, available at http:\/\/www.cs.kun.nl\/~freek\/mizar\/by.dvi"},{"key":"CR27","unstructured":"Wiedijk, F. (2002) Estimating the cost of a standard library for a mathematical proof checker, http:\/\/www.cs.kun.nl\/~freek\/notes"},{"key":"CR28","doi-asserted-by":"crossref","unstructured":"Wiedijk, F. (2003) Comparing mathematical provers, in A. Asperti, B. Buchberger and J. Davenport (eds.), Mathematical Knowledge Management, Proceedings of MKM 2003, LNCS 2594, pp. 188?202.","DOI":"10.1007\/3-540-36469-2_15"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-6245-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-004-6245-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-6245-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:45Z","timestamp":1559265705000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-004-6245-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,10]]},"references-count":28,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2004,10]]}},"alternative-id":["6245"],"URL":"https:\/\/doi.org\/10.1007\/s10817-004-6245-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,10]]}}}