{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:13Z","timestamp":1761611173322},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1992,6,1]],"date-time":"1992-06-01T00:00:00Z","timestamp":707356800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1992,6]]},"DOI":"10.1007\/bf02341853","type":"journal-article","created":{"date-parts":[[2006,3,15]],"date-time":"2006-03-15T05:59:53Z","timestamp":1142402393000},"page":"311-344","source":"Crossref","is-referenced-by-count":11,"title":["Gazing: An approach to the problem of definition and lemma use"],"prefix":"10.1007","volume":"8","author":[{"given":"Dave","family":"Barker-Plummer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF02341853_CR1","unstructured":"Bledsoe, W. W., \u2018The UT interactive prover\u2019, Memo ATP-17B, Mathematics Department, University of Texas, April 1983."},{"key":"BF02341853_CR2","unstructured":"Bledsoe, W. W. and Tyson, M., \u2018The UT interactive prover\u2019, Memo ATP-17, Mathematics Department, University of Texas, May 1975."},{"key":"BF02341853_CR3","unstructured":"Boyer, R. S. and Moore, J. S.,A Computational Logic. ACM Monograph Series, Academic Press, 1979."},{"key":"BF02341853_CR4","unstructured":"Bundy, A., \u2018Finding a common currency \u2014 a new proof plan\u2019. Internal Note 159, Department of Artificial Intelligence, University of Edinburgh, January 1983."},{"key":"BF02341853_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(88)90030-6","volume":"35","author":"D. Cvetkovic","year":"1988","unstructured":"CvetkovicD. and PevacI., \u2018Man-machine theorem proving in graph theory\u2019,Artificial Intelligence 35, 1\u201323 (1988).","journal-title":"Artificial Intelligence"},{"key":"BF02341853_CR6","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/0004-3702(72)90051-3","volume":"3","author":"R. E. Fikes","year":"1972","unstructured":"FikesR. E., HartP. E., and NilssonN. J., \u2018Learning and executing generalized robot plans\u2019,Artificial Intelligence 3, 251\u2013288 (1972).","journal-title":"Artificial Intelligence"},{"key":"BF02341853_CR7","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0004-3702(71)90010-5","volume":"2","author":"R. E. Fikes","year":"1971","unstructured":"FikesR. E. and NilssonN. J., \u2018Strips: A new approach to the application of theorem proving to problem solving\u2019,Artificial Intelligence 2, 189\u2013208 (1971).","journal-title":"Artificial Intelligence"},{"key":"BF02341853_CR8","unstructured":"Halmos, P.,Naive Set Theory. Van Nostrand. 1960."},{"key":"BF02341853_CR9","unstructured":"Kleene, S. C.,Mathematical Logic, John Wiley and Sons, Inc., 1967."},{"key":"BF02341853_CR10","unstructured":"Minsky, M., \u2018Steps towards artificial intelligence\u2019, in:Computers and Thought, McGraw Hill, 1963, pp. 406\u2013450."},{"key":"BF02341853_CR11","doi-asserted-by":"crossref","unstructured":"Plaisted, D. A., \u2018Abstraction mappings in mechanical theorem proving\u2019, in: Bibel, W. and Kowalski, B., Editors,5th CADE, 5th Conference on Automated Deduction, 1980, pp. 264\u2013280.","DOI":"10.1007\/3-540-10009-1_21"},{"key":"BF02341853_CR12","unstructured":"Plummer, D.,Gazing: A Technique for Controlling the Use of Rewrite Rules. Ph.D. thesis, Department of Artificial Intelligence, University of Edinburgh, May 1988."},{"key":"BF02341853_CR13","doi-asserted-by":"crossref","unstructured":"Robinson, J. A., \u2018A machine-oriented logic based on the resolution principle\u2019,ACM 12, 1965.","DOI":"10.1145\/321250.321253"},{"key":"BF02341853_CR14","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0004-3702(74)90026-5","volume":"5","author":"E. D. Sacerdoti","year":"1974","unstructured":"SacerdotiE. D., \u2018Planning in a hierarchy of abstracton spaces\u2019,Artificial Intelligence 5, 115\u2013135 (1974).","journal-title":"Artificial Intelligence"},{"key":"BF02341853_CR15","unstructured":"Sacerdoti, E. D.,A Structure for Plans and Behavior, Artificial Intelligence Series, Elsevier Computer Science Library, 1977."},{"key":"BF02341853_CR16","doi-asserted-by":"crossref","unstructured":"Siekmann, J., \u2018Universal unification\u2019, inProceedings of 7th CADE, Conference on Automated Deduction, 1984.","DOI":"10.1007\/978-0-387-34768-4_1"},{"key":"BF02341853_CR17","unstructured":"Sigler, L. E.,Exercises in Set Theory. Van Nostrand Mathematical Studies. Van Nostrand, 1966."},{"key":"BF02341853_CR18","unstructured":"Suppes, S.,Introduction to Logic, The University Series in Undergraduate Mathematics. D. Van Nostrand Company, Inc., 1957."},{"key":"BF02341853_CR19","doi-asserted-by":"crossref","unstructured":"Wos, L., \u2018The problem of definition expansion and contraction\u2019,J. Automated Reasoning 3 (1987).","DOI":"10.1007\/BF00247438"},{"key":"BF02341853_CR20","volume-title":"Automated Reasoning: 33 Basic Research Problems","author":"L. Wos","year":"1988","unstructured":"WosL.,Automated Reasoning: 33 Basic Research Problems. Prentice Hall, Englewood Cliffs, N.J. 1988."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02341853.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02341853\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02341853","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T21:14:04Z","timestamp":1557954844000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02341853"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,6]]},"references-count":20,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1992,6]]}},"alternative-id":["BF02341853"],"URL":"https:\/\/doi.org\/10.1007\/bf02341853","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,6]]}}}