{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T18:26:29Z","timestamp":1649096789014},"reference-count":22,"publisher":"World Scientific Pub Co Pte Lt","issue":"02","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Patt. Recogn. Artif. Intell."],"published-print":{"date-parts":[[1999,3]]},"abstract":"<jats:p> Automated theorem provers use search strategies. Unfortunately, there is no unique strategy which is uniformly successful on all problems. This motivates us to apply different strategies in parallel, in a competitive manner. In this paper, we discuss properties, problems, and perspectives of strategy parallelism in theorem proving. We develop basic concepts like the complementarity and the overlap value of strategy sets. Some of the problems such as initial strategy selection and run-time strategy exchange are discussed in more detail. The paper also contains the description of an implementation of a strategy parallel theorem prover (p-SETHEO) and an experimental evaluation. <\/jats:p>","DOI":"10.1142\/s0218001499000136","type":"journal-article","created":{"date-parts":[[2003,4,24]],"date-time":"2003-04-24T01:59:35Z","timestamp":1051149575000},"page":"219-245","source":"Crossref","is-referenced-by-count":4,"title":["STRATEGY PARALLELISM IN AUTOMATED THEOREM PROVING"],"prefix":"10.1142","volume":"13","author":[{"given":"ANDREAS","family":"WOLF","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Informatik der Technischen Universit\u00e4t M\u00fcnchen, D\u201380290 M\u00fcnchen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"REINHOLD","family":"LETZ","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik der Technischen Universit\u00e4t M\u00fcnchen, D\u201380290 M\u00fcnchen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"reference":[{"key":"p_2","first-page":"272","volume":"722","author":"Bonacina M. P.","year":"1993","journal-title":"Proc. DISCO-93"},{"key":"p_4","first-page":"57","volume":"1249","author":"Dahn B. I.","year":"1997","journal-title":"Proc. CADE-14"},{"key":"p_5","first-page":"58","author":"Dahn B. I.","year":"1997","journal-title":"Proc. FTP-97, RISC Linz, Austria"},{"key":"p_7","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005879229581"},{"key":"p_8","first-page":"62","volume":"1104","author":"Denzinger J.","year":"1996","journal-title":"Proc. CADE-13"},{"key":"p_9","first-page":"65","volume":"1249","author":"Fischer B.","year":"1997","journal-title":"Proc. CADE-14"},{"key":"p_11","first-page":"1","author":"Fuchs M.","year":"1997","journal-title":"Proc. 10th Int. Florida AI Research Society Conf., Florida AI Research Society"},{"key":"p_14","first-page":"778","volume":"814","author":"Goller C.","year":"1994","journal-title":"Proc. CADE-12"},{"key":"p_15","first-page":"13","author":"Honigmann T.","year":"1998","journal-title":"Proc. ALV-98, Munich Univ. of Technology, Computer Science Dept."},{"key":"p_17","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881947"},{"key":"p_18","doi-asserted-by":"publisher","DOI":"10.1007\/BF00244282"},{"key":"p_20","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005843632307"},{"key":"p_21","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005808119103"},{"key":"p_23","first-page":"753","volume":"607","author":"Reif W.","year":"1992","journal-title":"Proc. CADE11"},{"key":"p_24","first-page":"44","volume":"449","author":"Schumann J.","year":"1990","journal-title":"Proc. CADE-10"},{"key":"p_25","first-page":"484","volume":"814","author":"Sturgill D. B.","year":"1994","journal-title":"Proc. CADE-12"},{"key":"p_26","first-page":"252","volume":"814","author":"Sutcliffe G.","year":"1994","journal-title":"Proc. CADE-12"},{"key":"p_27","first-page":"2","volume":"18","author":"Suttner C.","year":"1997","journal-title":"JAR"},{"key":"p_28","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/B978-0-444-81704-4.50015-6","author":"Suttner C.","year":"1994","journal-title":"Parallel Processing for Artificial Intelligence, Elsevier"},{"key":"p_30","first-page":"427","volume":"1421","author":"Tammet T.","year":"1998","journal-title":"Proc. CADE-15"},{"key":"p_31","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005812220011"},{"key":"p_32","first-page":"129","volume":"24","author":"Wolf A.","year":"1997","journal-title":"T. Schnekenburger and G. Stellner, Teubner-Texte zur Informatik"}],"container-title":["International Journal of Pattern Recognition and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218001499000136","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T16:36:52Z","timestamp":1565195812000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218001499000136"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,3]]},"references-count":22,"journal-issue":{"issue":"02","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[1999,3]]}},"alternative-id":["10.1142\/S0218001499000136"],"URL":"https:\/\/doi.org\/10.1142\/s0218001499000136","relation":{},"ISSN":["0218-0014","1793-6381"],"issn-type":[{"value":"0218-0014","type":"print"},{"value":"1793-6381","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,3]]}}}