{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:07Z","timestamp":1761611107620,"version":"3.41.0"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2002,9]]},"DOI":"10.1023\/a:1021939521172","type":"journal-article","created":{"date-parts":[[2003,3,21]],"date-time":"2003-03-21T23:56:29Z","timestamp":1048290989000},"page":"253-275","source":"Crossref","is-referenced-by-count":23,"title":["Automated Proof Construction in Type Theory Using Resolution"],"prefix":"10.1007","volume":"29","author":[{"given":"Marc","family":"Bezem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dimitri","family":"Hendriks","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans","family":"de Nivelle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5109778_CR1","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. and 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":"5109778_CR2","doi-asserted-by":"crossref","unstructured":"Bezem, M., Hendriks, D. and de Nivelle, H.: Automated proof construction in type theory using resolution, in D. McAllester (ed.), Proceedings CADE 17, Lecture Notes in Comput. Sci. 1831, Springer-Verlag, 2000, pp. 148\u2013163.","DOI":"10.1007\/10721959_10"},{"key":"5109778_CR3","unstructured":"www.mpi-sb.mpg.de\/~bliksem."},{"key":"5109778_CR4","doi-asserted-by":"crossref","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures, in M. Abadi and T. Ito (eds), Theoretical Aspects of Computer Software (TACS), Lecture Notes in Comput. Sci. 1281, Springer-Verlag, 1997, pp. 515\u2013529.","DOI":"10.1007\/BFb0014565"},{"key":"5109778_CR5","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. G. de Bruijn","year":"1972","unstructured":"de Bruijn, N. G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, Indag. Math. 34 (1972), 381\u2013392.","journal-title":"Indag. Math"},{"key":"5109778_CR6","unstructured":"G\u00fcnzel, B.: Logik und das Auswahlaxiom, Diplomarbeit, Fakult\u00e4t f\u00fcr Mathematik und Informatik der Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, 2000."},{"key":"5109778_CR7","unstructured":"Hendriks, D.: Clausification of first-order formulae, representation & correctness in type theory, Master's thesis, Utrecht University, 1998."},{"key":"5109778_CR8","unstructured":"Hendriks, D.: Proof reflection in Coq, Artificial Intelligence Preprint Series 28, Dept. of Philosophy, Utrecht University, 2001."},{"key":"5109778_CR9","unstructured":"www.phil.uu.nl\/~hendriks\/coq\/blinc."},{"key":"5109778_CR10","doi-asserted-by":"crossref","unstructured":"Huang, X.: Translating machine-generated resolution proofs into ND-proofs at the assertion level, in Proceedings of PRICAI-96, 1996, pp. 399\u2013410.","DOI":"10.1007\/3-540-61532-6_34"},{"issue":"4","key":"5109778_CR11","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems, J. ACM\n27(4) (1980), 797\u2013821.","journal-title":"J. ACM"},{"key":"5109778_CR12","first-page":"311","volume":"1690","author":"J. Hurd","year":"1999","unstructured":"Hurd, J.: Integrating Gandalf and HOL, in Proceedings TPHOL's 99, Lecture Notes in Comput. Sci. 1690, Springer-Verlag, 1999, pp. 311\u2013321.","journal-title":"Proceedings TPHOL's 99"},{"key":"5109778_CR13","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"W. McCune","year":"2000","unstructured":"McCune, W. and Shumsky, O.: IVY: A preprocessor and proof checker for first-order logic, in M. Kaufmann, P. Manolios and J Moore (eds), Computer-Aided Reasoning: ACL2 Case Studies, Chapter 16, Kluwer Academic Publishers, Amsterdam, 2000."},{"key":"5109778_CR14","first-page":"499","volume-title":"Handbook of Logic in Artificial Intelligence","author":"G. Nadathur","year":"1998","unstructured":"Nadathur, G. and Miller, D.: Higher-order logic programming, in D. Gabbay et al. (eds), Handbook of Logic in Artificial Intelligence, Vol. 5, Clarendon Press, Oxford, 1998, pp. 499\u2013590."},{"key":"5109778_CR15","doi-asserted-by":"crossref","unstructured":"Nguyen, Q.-H.: Certifying term rewriting proofs in ELAN, Electronic Notes in Theoretical Computer Science, Vol. 59.4, Elsevier, 2001, 21 pages.","DOI":"10.1016\/S1571-0661(04)00295-6"},{"key":"5109778_CR16","unstructured":"www.ags.uni-sb.de\/~omega\/."},{"key":"5109778_CR17","first-page":"394","volume":"170","author":"F. Pfenning","year":"1984","unstructured":"Pfenning, F.: Analytic and non-analytic proofs, in Proceedings CADE 7, Lecture Notes in Comput. Sci. 170, Springer-Verlag, 1984, pp. 394\u2013413.","journal-title":"Proceedings CADE 7"},{"key":"5109778_CR18","doi-asserted-by":"crossref","unstructured":"Schwichtenberg, H.: Logic and the Axiom of Choice, in Logic Colloquium 78, pp. 351\u2013356.","DOI":"10.1016\/S0049-237X(08)71634-3"},{"key":"5109778_CR19","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1023\/A:1006393501098","volume":"24","author":"G. Sutcliffe","year":"2000","unstructured":"Sutcliffe, G.: The CADE-16 ATP system competition, J. Automated Reasoning\n24 (2000), 371\u2013396.","journal-title":"J. Automated Reasoning"},{"key":"5109778_CR20","first-page":"265","volume":"1158","author":"J. Smith","year":"1995","unstructured":"Smith, J. and Tammet, T.: Optimized encodings of fragments of type theory in first-order logic, in Proceedings Types 95, Lecture Notes in Comput. Sci. 1158, Springer-Verlag, 1995, pp. 265\u2013287.","journal-title":"Proceedings Types 95"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021939521172.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021939521172\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021939521172.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:33:31Z","timestamp":1749123211000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021939521172"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":20,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2002,9]]}},"alternative-id":["5109778"],"URL":"https:\/\/doi.org\/10.1023\/a:1021939521172","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2002,9]]}}}