{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:37:19Z","timestamp":1725493039956},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422549"},{"type":"electronic","value":"9783540457442"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45744-5_23","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T17:02:07Z","timestamp":1193418127000},"page":"318-324","source":"Crossref","is-referenced-by-count":0,"title":["A Second-Order Theorem Prover Applied to Circumscription"],"prefix":"10.1007","author":[{"given":"Michael","family":"Beeson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,8]]},"reference":[{"key":"23_CR1","unstructured":"Beeson, M., Implementing circumscription using second-order unification, http:\/\/www.mathcs.sjsu.edu\/faculty\/beeson\/Papers\/pubs.html"},{"key":"23_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundations of Constructive Mathematics","author":"M. Beeson","year":"1985","unstructured":"Beeson, M., Foundations of Constructive Mathematics, Springer-Verlag, Berlin\/ Heidelberg\/ New York (1985)."},{"key":"23_CR3","unstructured":"Beeson, M., Unification in Lambda Calculus with if-then-else, in: Kirchner, C., and Kirchner, H. (eds.), Automated Deduction-CADE-15. 15th International Conference on Automated Deduction, Lindau, Germany, July 1998 Proceedings, pp. 96\u2013111, Lecture Notes in Artificial Intelligence 1421, Springer-Verlag (1998)."},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Beeson, M., Automatic generation of epsilon-delta proofs of continuity, in: Calmet, Jacques, and Plaza, Jan (eds.) Artificial Intelligence and Symbolic Computation: International Conference AISC-98, Plattsburgh, New York, USA, September 1998 Proceedings, pp. 67\u201383. Springer-Verlag (1998).","DOI":"10.1007\/BFb0055903"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Beeson, M., Automatic generation of a proof of the irrationality of e, in Armando, A., and Jebelean, T. (eds.): Proceedings of the Calculumus Workshop, 1999, Electronic Notes in Theoretical Computer Science 23 3, 2000. Elsevier. Available at http:\/\/www.elsevier.nl\/locate\/entcs . This paper has also been accepted for publication in a special issue of Journal of Symbolic Computation which should appear in the very near future.","DOI":"10.1016\/S1571-0661(05)80613-9"},{"key":"23_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/BFb0038693","volume-title":"Extensions of Logic Programming","author":"M. Beeson","year":"1991","unstructured":"Beeson, M., Some applications of Gentzen\u2019s proof theory to automated deduction, in P. Schroeder-Heister (ed.), Extensions of Logic Programming, Lecture Notes in Computer Science 475 101\u2013156, Springer-Verlag (1991)."},{"key":"23_CR7","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1005722130532","volume":"18","author":"P. Doherty","year":"1997","unstructured":"Doherty, P., Lukaszewicz, W., And Szalas, A., Computing circumscription revisited: a reduction algorithm, J. Automated Reasoning 18, 297\u2013334 (1997).","journal-title":"J. Automated Reasoning"},{"key":"23_CR8","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0004-3702(89)90026-X","volume":"39","author":"M. L. Ginsberg","year":"1989","unstructured":"Ginsberg, M. L., A circumscriptive theorem prover, Artificial Intelligence 39 pp. 209\u2013230, 1989.","journal-title":"Artificial Intelligence"},{"key":"23_CR9","unstructured":"Introduction to Metamathetics, van Nostrand, Princeton, N.J. (1950)."},{"key":"23_CR10","first-page":"121","volume":"1","author":"V. Lifschitz","year":"1985","unstructured":"Lifschitz, V., Computing circumscription, in: Proceedings of the 9th International Joint Conference on Artificial Intelligence, volume 1, pages 121\u2013127, 1985.","journal-title":"Proceedings of the 9th International Joint Conference on Artificial Intelligence"},{"issue":"1-2","key":"23_CR11","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0004-3702(80)90011-9","volume":"13","author":"J. McCarthy","year":"1980","unstructured":"McCarthy, J., Circumscription, a form of non-monotonic reasoning, Artificial Intelligence, 13 (1-2), pp. 27\u201339, 1980.","journal-title":"Artificial Intelligence"},{"key":"23_CR12","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0004-3702(89)90067-2","volume":"38","author":"T. Przymusinski","year":"1991","unstructured":"Przymusinski, T., An algorithm to compute circumscription, Artigficial Intelligence, 38, pp. 49\u201373, 1991.","journal-title":"Artigficial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45744-5_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T10:48:21Z","timestamp":1684061301000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45744-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422549","9783540457442"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-45744-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]}}}