{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:21Z","timestamp":1725663501722},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_212","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:22:18Z","timestamp":1330251738000},"page":"726-730","source":"Crossref","is-referenced-by-count":1,"title":["The GAZER theorem prover"],"prefix":"10.1007","author":[{"given":"Dave","family":"Barker-Plummer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alex","family":"Rothenberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"62_CR1","unstructured":"W.W. Bledsoe. The Ut interactive prover. Memo ATP-17B, Mathematics Department, University of Texas, April 1983."},{"key":"62_CR2","unstructured":"R.S. Boyer and J S. Moore. A Computational Logic. ACM Monograph Series. Academic Press, 1979."},{"key":"62_CR3","volume-title":"Technical Report CS-1989-15","author":"D. Barker-Plummer","year":"1989","unstructured":"D. Barker-Plummer. The gazer theorem prover: Description and users guide. Technical Report CS-1989-15, Department of Computer Science, Duke University, Durham, North Carolina, 27706, USA, 1989."},{"key":"62_CR4","volume-title":"Technical Report CS-1989-13","author":"D. Barker-Plummer","year":"1989","unstructured":"D. Barker-Plummer. Gazing: An approach to the problem of definition expansion. Technical Report CS-1989-13, Department of Computer Science, Duke University, Durham, North Carolina, 27706, USA, 1989. To Appear in the Journal of Automated Reasoning."},{"key":"62_CR5","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/S0004-3702(78)80017-4","volume":"10","author":"F.M. Brown","year":"1978","unstructured":"F.M. Brown. Towards the automation of set theory and its logic. Artificial Intelligence, 10:281\u2013316, 1978.","journal-title":"Artificial Intelligence"},{"key":"62_CR6","unstructured":"W.W. Bledsoe and M. Tyson. The Ut interactive prover. Memo ATP-17, Mathematics Department, University of Texas, May 1975."},{"key":"62_CR7","unstructured":"A. Bundy. Finding a common currency \u2014 a new proof plan. Internal Note 159, Department of Artificial Intelligence, University of Edinburgh., January 1983."},{"key":"62_CR8","unstructured":"G. Gentzen. Untersuchen \u00fcber das logische schliessen [investigations into logical deduction]. In M.E. Szabo, editor, The Collected Papers of Gerhard Gentzen, chapter 3, pages 68\u2013131. North-Holland, 1969. First appeared in 1935 as an article in Mathemaiische Zeitschrift 39. This work was accepted as Gentzen's Inaugural Dissertation at the University of G\u00f6ttingen."},{"key":"62_CR9","unstructured":"D. Plummer. Gazing: A Technique for Controlling the Use of Rewrite Rules. PhD thesis, Department of Artificial Intelligence, University of Edinburgh, May 1988."},{"key":"62_CR10","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0004-3702(74)90026-5","volume":"5","author":"E.D. Sacerdoti","year":"1974","unstructured":"E.D. Sacerdoti. Planning in a hierarchy of abstraction spaces. Artificial Intelligence, 5:115\u2013135, 1974.","journal-title":"Artificial Intelligence"},{"key":"62_CR11","doi-asserted-by":"crossref","unstructured":"L. Wos. The problem of definition expansion and contraction. Journal of Automated Reasoning, 3(4), December 1987.","DOI":"10.1007\/BF00247438"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_212.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:33:03Z","timestamp":1619573583000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_212"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_212","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}