{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:02Z","timestamp":1749125162272},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_10","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"148-163","source":"Crossref","is-referenced-by-count":6,"title":["Automated Proof Construction in Type Theory Using Resolution"],"prefix":"10.1007","author":[{"given":"Marc","family":"Bezem","sequence":"first","affiliation":[]},{"given":"Dimitri","family":"Hendriks","sequence":"additional","affiliation":[]},{"given":"Hans","family":"de Nivelle","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Bliksem is available at http:\/\/www.mpi-sb.mpg.de\/~bliksem"},{"key":"10_CR2","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. Bruijn de","year":"1972","unstructured":"de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation. Indagationes Mathematicae\u00a034, 381\u2013392 (1972)","journal-title":"Indagationes Mathematicae"},{"key":"10_CR3","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Filli\u00e2tre, J.-C., Gim\u00e9nez, E., Herbelin, H., Huet, G., Mu\u00f1ez, C., Murthy, C., Parent, C., Paulin-Mohring, C., Sa\u00efbi, A., Werner, B.: The Coq Proof Assistant Reference Manual, version 6.2.4. INRIA (1998), Available at: ftp.inria.fr\/INRIA\/coq\/V6.2.4\/doc\/Reference-Manual.ps"},{"key":"10_CR4","unstructured":"Hendriks, D.: Clausification of First-Order Formulae, Representation & Correctness in Type Theory. Master\u2019s Thesis. Utrecht University (1998), http:\/\/www.phil.uu.nl\/~hendriks\/thesis.ps.gz"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/3-540-61532-6_34","volume-title":"PRICAI \u201996: Topics in Artificial Intelligence","author":"X. Huang","year":"1996","unstructured":"Huang, X.: Translating machine-generated resolution proofs into ND-proofs at the assertion level. In: Foo, N.Y., G\u00f6bel, R. (eds.) PRICAI 1996. LNCS, vol.\u00a01114, pp. 399\u2013410. Springer, Heidelberg (1996)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 311\u2013321. Springer, Heidelberg (1999)"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"McCune,W., Shumsky,O.: IVY: A preprocessor and proof checker for firstorder logic.(Preprint ANL\/MCS-P775-0899) Argonne National Laboratory, Argonne IL (1999)","DOI":"10.1007\/978-1-4757-3188-0_16"},{"key":"10_CR8","first-page":"499","volume-title":"Handbook of logic in artificial intelligence","author":"G. Nadathur","year":"1998","unstructured":"Nadathur, G., Miller, D.: Higher-order logic programming. In: Gabbay, D. (ed.) Handbook of logic in artificial intelligence, vol.\u00a05, pp. 499\u2013590. Clarendon Press, Oxford (1998)"},{"key":"10_CR9","unstructured":"Omega can be found on, http:\/\/www.ags.uni-sb.de\/~omega\/"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/BFb0047133","volume-title":"7th International Conference on Automated Deduction","author":"F. Pfenning","year":"1984","unstructured":"Pfenning, F.: Analytic and non-analytic proofs. In: Shostak, R.E. (ed.) CADE 1984. LNCS, vol.\u00a0170, pp. 394\u2013413. Springer, Heidelberg (1984)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BFb0020597","volume-title":"Types for Proofs and Programs","author":"J. Smith","year":"1996","unstructured":"Smith, J., Tammet, T.: Optimized encodings of fragments of type theory in first-order logic. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 265\u2013287. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,10]],"date-time":"2023-05-10T07:10:19Z","timestamp":1683702619000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/10721959_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}