{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:30Z","timestamp":1749124050307,"version":"3.32.0"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"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":[[1994]]},"DOI":"10.1007\/bf00881946","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:25:12Z","timestamp":1104002712000},"page":"283-296","source":"Crossref","is-referenced-by-count":9,"title":["METEOR: Exploring model elimination theorem proving"],"prefix":"10.1007","volume":"13","author":[{"given":"Owen","family":"Astrachan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"Ali, K. A. M. and Karlsson, R.: The muse or-parallel Prolog model and its performance, in S. Debray and M. Hermenegildo (eds),Proc. North American Conference on Logic Programming, 1990, pp. 757?776."},{"key":"CR2","unstructured":"Astrachan, O. L.: Investigations in model elimination based theorem proving, PhD thesis, Duke University, 1992."},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Astrachan, O. L. and Loveland, D. W.: METEORs: High performance theorem provers using model elimination, in R. S. Boyer (ed.),Automated Reasoning: Essays in Honor of Woody Bledsoe, Kluwer Academic Publishers, 1991.","DOI":"10.1007\/978-94-011-3488-0_2"},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"Astrachan, O. L. and Sickel, M. E.: Caching and lemmaizing in model elimination theorem provers. Technical Report 513, SRI International, Menlo Park, Ca., 1991.","DOI":"10.1007\/3-540-55602-8_168"},{"key":"CR5","volume-title":"Proc. 11th International Conference on Automated Deduction","author":"O. L. Astrachan","year":"1992","unstructured":"Astrachan, O. L. and Stickel, M. E.: Caching and lemmaizing in model elimination theorem provers, in Deepak Kapur (ed.),Proc. 11th International Conference on Automated Deduction, Springer-Verlag, Berlin, 1992."},{"key":"CR6","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures, vol. II: Rewriting Techniques","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., and Plaisted, D. A.: Completion without failure, in H. A\ufffdtKaci and M. Nivat (eds),Resolution of Equations in Algebraic Structures, vol. II: Rewriting Techniques, Academic Press, New York, 1989, pp. 1?30."},{"key":"CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00263762","volume":"9","author":"R. Bayer","year":"1977","unstructured":"Bayer, R. and Schkolnick, M.: Concurrency of operations in b-trees,Acta Informatica 9 (1977), 1?21.","journal-title":"Acta Informatica"},{"issue":"3","key":"CR8","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W. W. Bledsoe","year":"1990","unstructured":"Bledsoe, W. W.: Challenge problems in elementary calculus,J. Automated Reasoning 6(3) (1990), 341?359.","journal-title":"J. Automated Reasoning"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Bonacina, M. P. and Hsiang, J.: Distributed deduction by clause-diffusion: The Aquarius prover, in Alfonso Miola (ed.),Proc. International Symposium on Design and Implementation of Symbolic Computation Systems, Lecture Notes in Comput. Sci. 722, Springer-Verlag, 1993, pp. 272?287.","DOI":"10.1007\/BFb0013183"},{"key":"CR10","unstructured":"Bose, S., Clarke, E., Long, D. E., and Michaylov, S.: Parthenon: A parallel theorem prover for non-Horn clauses, inProc. Symposium on Logic in Computer Science, 1989."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/BF00244281","volume":"8","author":"S Bose","year":"1992","unstructured":"Bose, S, Clarke, E., Long, D. E., and Michaylov, S.: Parthenon: A parallel theorem prover for non-Horn clauses,J. Automated Reasoning 8 (1992), 153?181.","journal-title":"J. Automated Reasoning"},{"key":"CR12","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems,Theoretical Computer Science 17 (1982), 279?301.","journal-title":"Theoretical Computer Science"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/BF00289064","volume":"14","author":"C. S. Ellis","year":"1980","unstructured":"Ellis, C. S.: Concurrent search and insertion in 2?3 trees,Acta Informatica 14 (1980), 63?86.","journal-title":"Acta Informatica"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1145\/321796.321807","volume":"21","author":"S. Fleisig","year":"1974","unstructured":"Fleisig, S., Loveland, D., Smiley, A., and Yarmash, D.: An implementation of the model elimination proof procedure,JACM 21 (1974), 124?139.","journal-title":"JACM"},{"key":"CR15","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/BF00263447","volume":"8","author":"A. Jindal","year":"1992","unstructured":"Jindal, A., Overbeek, R., and Kabat, W. C.: Exploitation of parallel processing for implementing high-performance deduction systems,J. Automated Reasoning 8 (1992), 23?38.","journal-title":"J. Automated Reasoning"},{"key":"CR16","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"R. E. Korf","year":"1985","unstructured":"Korf, R. E.: Depth-first iterative deepening: An optimal admissible tree search,Artificial Intelligence 27 (1985), 97?109.","journal-title":"Artificial Intelligence"},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"Kotz, D. and Ellis, C. S.: Evaluation of concurrent pools, inProc. 9th International Conference on Distributed Computing Systems, 1989, pp. 378?385.","DOI":"10.1109\/ICDCS.1989.37968"},{"issue":"11","key":"CR18","doi-asserted-by":"crossref","first-page":"806","DOI":"10.1145\/359863.359878","volume":"20","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Concurrent reading and writing,Communications of the ACM 20(11) (1977), 806?811.","journal-title":"Communications of the ACM"},{"key":"CR19","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R Letz","year":"1992","unstructured":"Letz, R, Bayerl, S., Schumann, J., and Bibel, W.: SETHEO ? a high-performance theorem prover,J. Automated Reasoning 8 (1992), 183?212.","journal-title":"J. Automated Reasoning"},{"key":"CR20","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. W. Loveland","year":"1978","unstructured":"Loveland, D. W.:Automated Theorem Proving: A Logical Basis, North-Holland, Amsterdam, 1978."},{"issue":"2","key":"CR21","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D. W. Loveland","year":"1968","unstructured":"Loveland, D. W.: Mechanical theorem proving by model elimination,JACM 15(2) (1968), 236?251.","journal-title":"JACM"},{"issue":"3","key":"CR22","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D. W. Loveland","year":"1969","unstructured":"Loveland, D. W.: A simplified format for the model elimination procedure,JACM 16(3) (1969), 349?363.","journal-title":"JACM"},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"Lusk, E., McCune, W. W., and Slaney, J.: Roo: A parallel theorem prover, in Deepak Kapur (ed.),Proc. 11th International Conference on Automated Deduction, Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_213"},{"key":"CR24","doi-asserted-by":"crossref","unstructured":"McCune, W.: Otter 2.0. In Mark Stickel (ed.),Proc. 10th International Conference on Automated Deduction, Springer-Verlag, 1990, pp. 663?664.","DOI":"10.1007\/3-540-52885-7_131"},{"issue":"4","key":"CR25","doi-asserted-by":"crossref","first-page":"1130","DOI":"10.1137\/0215082","volume":"15","author":"U. Manber","year":"1986","unstructured":"Manber, U.: On maintaining dynamic information in a concurrent environment,SIAM J. Computing 15(4) (1986), 1130?1142.","journal-title":"SIAM J. Computing"},{"issue":"3","key":"CR26","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. Plaisted","year":"1988","unstructured":"Plaisted, D.: Non-Horn clause logic programming without contrapositives,J. Automated Reasoning 4(3) (1988), 287?325.","journal-title":"J. Automated Reasoning"},{"key":"CR27","doi-asserted-by":"crossref","unstructured":"Schumann, J. and Letz, R.: PARTHEO: A high performance parallel theorem prover, inProc. 10th International Conference on Automated Deduction, 1990, pp. 40?56.","DOI":"10.1007\/3-540-52885-7_78"},{"key":"CR28","unstructured":"Spencer, B.: Avoiding duplicate proofs, in S. Debray and M. Hermenegildo (eds),Proc. North American Conference on Logic Programming, 1990, pp. 569?584."},{"key":"CR29","doi-asserted-by":"crossref","unstructured":"Stevens, W. R.:UNIX Network Programming, Prentice-Hall, 1990.","DOI":"10.1145\/378570.378600"},{"issue":"4","key":"CR30","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/BF03037328","volume":"2","author":"M. E. Stickel","year":"1984","unstructured":"Stickel, M. E.: A Prolog technology theorem prover,New Generation Computing 2(4) (1984), 371?383.","journal-title":"New Generation Computing"},{"key":"CR31","doi-asserted-by":"crossref","unstructured":"Stickel, M. E.: A Prolog technology theorem prover: Implementation by an extended Prolog compiler, inProc. 8th International Conference on Automated Deduction, Springer-Verlag, 1986, pp. 573?587.","DOI":"10.1007\/3-540-16780-3_122"},{"key":"CR32","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"Stickel, M. E.: A Prolog technology theorem prover: Implementation by an extended Prolog compiler,J. Automated Reasoning 4 (1988), 343?380.","journal-title":"J. Automated Reasoning"},{"key":"CR33","unstructured":"Stickel, M. E. and Tyson, W. A.: An analysis of consecutively bounded depth-first search with applications in automated deduction, inProc. 9th International Joint Conference on Artificial Intelligence, 1985, pp. 1073?1075."},{"key":"CR34","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/BF00381144","volume":"3","author":"T. C. Wang","year":"1987","unstructured":"Wang, T. C., and Bledsoe, W. W.: Hierarchical deduction,J. Automated Reasoning 3 (1987), 35?77.","journal-title":"J. Automated Reasoning"},{"key":"CR35","unstructured":"Warren, D. H. D.: An abstract Prolog instruction set. Technical Report 309, SRI International, Menlo Park, Ca., 1983."},{"issue":"8","key":"CR36","doi-asserted-by":"crossref","first-page":"782","DOI":"10.1109\/TC.1976.1674697","volume":"C-25","author":"G. A. Wilson","year":"1976","unstructured":"Wilson, G. A. and Minker, J.: Resolution, refinements, and search strategies: A comparative study,IEEE Trans. Computers C-25(8) (1976), 782?801.","journal-title":"IEEE Trans. Computers"},{"key":"CR37","unstructured":"Wos, L.:Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, 1988."},{"key":"CR38","unstructured":"Wos, L and Overbeek, R.: Subsumption, a sometimes undervalued procedure, in J.-L. Lassez and G. Plotkin (eds),Computational Logic, Essays in Honor of Alan Robinson, MIT Press, 1991."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881946.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881946\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881946","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,21]],"date-time":"2024-12-21T17:46:56Z","timestamp":1734803216000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881946"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1994]]}},"alternative-id":["BF00881946"],"URL":"https:\/\/doi.org\/10.1007\/bf00881946","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1994]]}}}