{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:36Z","timestamp":1725494316505},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_15","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T15:53:07Z","timestamp":1194623587000},"page":"207-211","source":"Crossref","is-referenced-by-count":17,"title":["System Description: inka 5.0 - A Logic Voyager"],"prefix":"10.1007","author":[{"given":"Serge","family":"Autexier","sequence":"first","affiliation":[]},{"given":"Dieter","family":"Hutter","sequence":"additional","affiliation":[]},{"given":"Heiko","family":"Mantel","sequence":"additional","affiliation":[]},{"given":"Axel","family":"Schairer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"C. Benzm\u00fcller et al.: MEGA: Towards a mathematical assistant, In W. McCune (ed), CADE-14, Springer, LNAI 1249, 1997.","key":"15_CR1","DOI":"10.1007\/3-540-63104-6_23"},{"key":"15_CR2","series-title":"Lect Notes Comput Sci","volume-title":"CADE-8","author":"S. Biundo","year":"1986","unstructured":"S. Biundo, B. Hummel, D. Hutter, C. Walther: The Karlsruhe Induction Theorem Proving System. In J\u00f6rg H. Siekmann (ed), CADE-8, Springer, LNCS 230, 1986."},{"unstructured":"CoFi-task group on language design, ESPRIT working group 29432, EU, 1998. CoFI Webpage: http:\/\/www.brics.dk\/Projects\/CoFI\/","key":"15_CR3"},{"doi-asserted-by":"crossref","unstructured":"L. Damas, R. Milner: Principal type schemes for functional programs, Ann. ACM Symp. on Principles of Programming Languages (POPL), 1982.","key":"15_CR4","DOI":"10.1145\/582153.582176"},{"doi-asserted-by":"crossref","unstructured":"R. Harper, F. Honsell, G. Plotkin: A framework for defining logics, Journal of the Association for Computing Machinery, 40(1), 1993.","key":"15_CR5","DOI":"10.1145\/138027.138060"},{"unstructured":"D. Hutter, M. Kohlhase: Managing Structural Information by Higher-Order Colored Unification, Journal of Automated Reasoning, accepted, 1999.","key":"15_CR6"},{"unstructured":"D. Hutter et al.: Verification Support Environment (VSE), Journal of High Integrity Systems, Vol. 1, 1996.","key":"15_CR7"},{"doi-asserted-by":"crossref","unstructured":"D. Hutter, C. Sengler: inka-The Next Generation. In M. McRobbie, J. Slaney (ed), CADE-13, Springer, LNAI 1104, 1996.","key":"15_CR8","DOI":"10.1007\/3-540-61511-3_92"},{"doi-asserted-by":"crossref","unstructured":"D. Hutter: Guiding Induction Proofs, In M. Stickel (ed), CADE-10, Springer, LNAI 449, 1991.","key":"15_CR9","DOI":"10.1007\/3-540-52885-7_85"},{"doi-asserted-by":"crossref","unstructured":"D. Hutter: Coloring terms to control equational reasoning, Journal of Automated Reasoning, Vol. 18, 1997.","key":"15_CR10","DOI":"10.1023\/A:1005772217686"},{"unstructured":"Programming System Lab, Saarland University, Saarbr\u00fccken, 1998. The Oz Webpage: http:\/\/www.ps.uni-sb.de\/ns3\/oz\/","key":"15_CR11"},{"key":"15_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"L.C. Paulson: Isabelle, A Generic Theorem Prover, Springer, LNCS 828, 1994."},{"unstructured":"J. Siekmann et al.: A Distributed Graphical User Interface for the Interactive Proof System MEGA. In R. C. Backhouse (ed), UITP98, Eindhoven Technical University, Report 98-08, 1998.","key":"15_CR13"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,27]],"date-time":"2021-08-27T03:03:00Z","timestamp":1630033380000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}