{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:45Z","timestamp":1749182805377,"version":"3.41.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1997,12,1]],"date-time":"1997-12-01T00:00:00Z","timestamp":880934400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,12,1]],"date-time":"1997-12-01T00:00:00Z","timestamp":880934400000},"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":[[1997,12]]},"DOI":"10.1023\/a:1005885725562","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:56:21Z","timestamp":1040514981000},"page":"347-376","source":"Crossref","is-referenced-by-count":3,"title":["Nagging: A Distributed, Adversarial Search-Pruning Technique Applied to First-Order Inference"],"prefix":"10.1007","volume":"19","author":[{"given":"David","family":"Sturgill","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto Maria","family":"Segre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"136197_CR1","doi-asserted-by":"crossref","unstructured":"A\u00eft-Kaci, H.: Warren\u2019s Abstract Machine, MIT Press, 1991.","DOI":"10.7551\/mitpress\/7160.001.0001"},{"key":"136197_CR2","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, 1991, pp. 31\u201359.","DOI":"10.1007\/978-94-011-3488-0_2"},{"key":"136197_CR3","doi-asserted-by":"crossref","unstructured":"Astrachan, O. L. and Stickel, M. E.: Caching and lemmaizing in model elimination theorem provers, in D. Kapur (ed.), 11th Int. Conf. Autom. Deduction, Springer-Verlag, 1992, pp. 224\u2013238.","DOI":"10.1007\/3-540-55602-8_168"},{"issue":"1","key":"136197_CR4","first-page":"69","volume":"15","author":"N. Bhatnagar","year":"1994","unstructured":"Bhatnagar, N. and Mostow, J.: On-line learning from search failures, Machine Learning\n15(1) (1994), 69\u2013117.","journal-title":"Machine Learning"},{"issue":"2","key":"136197_CR5","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/BF00244281","volume":"8","author":"S. Bose","year":"1992","unstructured":"Bose, S., Clarke, E. M., Long, D. E. and Michaylov, S.: Parthenon: A parallel theorem prover for non-horn clauses, J. Automated Reasoning\n8(2) (1992), 153\u2013181.","journal-title":"J. Automated Reasoning"},{"key":"136197_CR6","doi-asserted-by":"crossref","unstructured":"Br\u00fcning, S.: Detecting non-provable goals, in Alan Bundy (ed.), 12th Int. Conf. Automated Deduction, Springer-Verlag, 1994, pp. 222\u2013236.","DOI":"10.1007\/3-540-58156-1_16"},{"key":"136197_CR7","unstructured":"Bruynooghe, M: Intelligent backtracking for an interpreter of horn clause logic programs, in B. D\u00f6m\u00f6lki and T. Gergely (eds), Math. Logic in Computer Science, North-Holland, 1978, pp. 215\u2013258."},{"key":"136197_CR8","unstructured":"Bundy, A.: The Computer Modelling of Mathematical Reasoning, Academic Press, 1983."},{"key":"136197_CR9","unstructured":"Chang, C-L. and Lee, R. C-T.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973."},{"key":"136197_CR10","unstructured":"Chang, J-H. and Despain, A. M.: Semi-intelligent backtracking of Prolog based on static data dependency analysis, in Proc. IEEE Symp. Logic Programming, IEEE Computer Society, 1985, pp. 10\u201321."},{"key":"136197_CR11","doi-asserted-by":"crossref","unstructured":"Clocksin, W. F.: Principles of the DelPhi parallel inference machine, Computer Journal(1987), 386\u2013392.","DOI":"10.1093\/comjnl\/30.5.386"},{"key":"136197_CR12","unstructured":"DeGroot, D.: Restricted and-parallelism, in Proc. Int. Conf. Fifth Generation Computer Systems, North-Holland, 1984, pp. 471\u2013478."},{"key":"136197_CR13","unstructured":"Delgado-Rannauro, S. A.: Stream and-parallel logic computational models, in P. Kacsuk and M. J. Wise (eds), Implementations of Distributed Prolog, John Wiley and Sons, 1992, pp. 239\u2013257."},{"key":"136197_CR14","unstructured":"Delgado-Rannauro, S. A.: Or-parallel logic computational models, in P. Kacsuk and M. J. Wise (eds), Implementations of Distributed Prolog, John Wiley and Sons, 1992, pp. 3\u201326."},{"key":"136197_CR15","doi-asserted-by":"crossref","unstructured":"Ertel, W.: Random competition: A simple but efficient method for parallelizing inference systems, in Parallelization in Inference Systems, Springer-Verlag, 1990, pp. 195\u2013209.","DOI":"10.1007\/3-540-55425-4_9"},{"key":"136197_CR16","doi-asserted-by":"crossref","unstructured":"Hermenegildo, M. V.: An abstract machine for restricted and-parallel execution of logic programs, in E. Shapiro (ed.), Third Int. Conf. Logic Programming, Springer-Verlag, 1986, pp. 25\u201339.","DOI":"10.1007\/3-540-16492-8_62"},{"key":"136197_CR17","first-page":"155","volume":"1","author":"H. Kautz","year":"1994","unstructured":"Kautz, H. and Selman, B.: An empirical evaluation of knowledge compilation by theory approximation, in Proc. AAAI-94, Vol. 1, MIT Press, 1994, pp. 155\u2013161.","journal-title":"Proc. AAAI-94"},{"issue":"1","key":"136197_CR18","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"R. Korf","year":"1985","unstructured":"Korf, R.: Depth-first iterative deepening: An optimal admissible tree search, Artificial Intelligence\n27(1) (1985), 97\u2013109.","journal-title":"Artificial Intelligence"},{"key":"136197_CR19","unstructured":"Kumar, V. and Lin, Y-J.: An intelligent backtracking scheme for Prolog, in Proc. IEEE Symposium on Logic Programming, IEEE Computer Society, 1987, pp. 406\u2013414."},{"key":"136197_CR20","unstructured":"Kurfe\u00df, F.: Potentiality of parallelism in logic, in Parallelization in Inference Systems, Springer-Verlag, 1990, pp. 3\u201325."},{"issue":"3","key":"136197_CR21","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"Letz, R., Mayr, K.and Goller, C.: Controlled integration of the cut rule into connection tableau calculi, J. Automated Reasoning\n13(3) (1994), 297\u2013337.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"136197_CR22","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S. and Bibel, W.: Setheo: A high-performance theorem prover, J. Automated Reasoning\n8(2) (1992), 183\u2013212.","journal-title":"J. Automated Reasoning"},{"key":"136197_CR23","first-page":"366","volume":"19","author":"D. W. Loveland","year":"1972","unstructured":"Loveland, D. W.: A unifying view of some linear herbrand procedures, J. Assoc. Computing Machinery\n19(1972), 366\u2013384.","journal-title":"J. Assoc. ComputingMachinery"},{"key":"136197_CR24","unstructured":"Loveland, D. W.: Automated Theorem Proving: A Logical Basis, North-Holland, 1978."},{"key":"136197_CR25","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/0004-3702(81)90015-1","volume":"16","author":"D. A. Plaisted","year":"1981","unstructured":"Plaisted, D. A.: Theorem proving with abstraction, Artificial Intelligence\n16(1981), 47\u2013108.","journal-title":"Artificial Intelligence"},{"key":"136197_CR26","doi-asserted-by":"crossref","unstructured":"Schumann, J., Letz, R. and Kurfess, F.: Tutorial on high-performance theorem provers: Efficient implementation and parallelism, in Mark E. Stickel (ed.), 10th Int. Conf. Automated Deduction, Springer-Verlag, 1990, Summary, p. 683.","DOI":"10.1007\/3-540-52885-7_145"},{"key":"136197_CR27","doi-asserted-by":"crossref","unstructured":"Schumann, J. M. and Letz, R.: Partheo: A high-performance parallel theorem prover, in Mark E. Stickel (ed.), 10th Int. Conf. Automated Deduction, Springer-Verlag, 1990, pp. 40\u201356.","DOI":"10.1007\/3-540-52885-7_78"},{"key":"136197_CR28","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BF00881901","volume":"11","author":"A. M. Segre","year":"1993","unstructured":"Segre, A. M. and Scharstein, D.: Bounded-overhead caching for definite-clause theorem proving, J. Automated Reasoning\n11(1993), 83\u2013113.","journal-title":"J. Automated Reasoning"},{"key":"136197_CR29","unstructured":"Segre, A. M. and Sturgill, D.: Using hundreds of workstations to solve first-order logic problems, in Proc. AAAI-94, MIT Press, 1994, pp. 187\u2013192."},{"key":"136197_CR30","first-page":"904","volume":"2","author":"B. Selman","year":"1991","unstructured":"Selman, B. and Kautz, H.: Knowledge compilation using Horn approximations, in Proc. AAAI-91, Vol. 2, 1991, pp. 904\u2013909.","journal-title":"Proc. AAAI-91"},{"key":"136197_CR31","doi-asserted-by":"crossref","first-page":"353","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\n4(1988), 353\u2013380.","journal-title":"J. Automated Reasoning"},{"key":"136197_CR32","unstructured":"Stickel, M. E. and Tyson, W. M.: An analysis of consecutively bounded depth-first search with applications in automated deduction, in Proc. Ninth Int. Joint Conf. Artificial Intelligence, 1985, pp. 1073\u20131075."},{"key":"136197_CR33","unstructured":"Sturgill, D.: Nagging: A New Approach to Parallel Search Pruning, PhD thesis, Cornell University, 1996."},{"key":"136197_CR34","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Suttner, C. and Yemenis, T.: The TPTP problem library, in Alan Bundy (ed.), 12th Int. Conf. Automated Deduction, Springer-Verlag, 1994, pp. 252\u2013266.","DOI":"10.1007\/3-540-58156-1_18"},{"key":"136197_CR35","doi-asserted-by":"crossref","unstructured":"Suttner, C. B. and Schumann, J.: Parallel automated theorem proving, in L. Kanal, V. Kumar, H. Kitano, and C. Suttner (eds), Parallel Processing for Artificial Intelligence I, Elsevier, 1993, pp. 209\u2013257.","DOI":"10.1016\/B978-0-444-81704-4.50015-6"},{"key":"136197_CR36","unstructured":"Warren, D. H. D.: An abstract Prolog instruction set, Technical Report 309, SRI International, 1983."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005885725562.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005885725562\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005885725562.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:24:00Z","timestamp":1749122640000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005885725562"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,12]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1997,12]]}},"alternative-id":["136197"],"URL":"https:\/\/doi.org\/10.1023\/a:1005885725562","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1997,12]]}}}