{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T11:31:21Z","timestamp":1648726281735},"reference-count":13,"publisher":"World Scientific Pub Co Pte Lt","issue":"01n02","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Artif. Intell. Tools"],"published-print":{"date-parts":[[2001,3]]},"abstract":"<jats:p> Automated theorem proving with connection tableau calculi imposes search problems in tremendous search spaces. In this paper, we present a new approach to search space reduction in connection tableau calculi. In our approach structurally similar parts of the search space are compressed by means of disjunctive constraints. We describe the necessary changes of the calculus, and we develop elaborate techniques for an efficient constraint processing. Moreover, we present an experimental evaluation of our approach. <\/jats:p>","DOI":"10.1142\/s0218213001000477","type":"journal-article","created":{"date-parts":[[2003,6,4]],"date-time":"2003-06-04T05:18:04Z","timestamp":1054703884000},"page":"181-198","source":"Crossref","is-referenced-by-count":0,"title":["AN AUTOMATED THEOREM PROVER BASED ON CONNECTION TABLEAU CALCULI WITH DISJUNCTIVE CONSTRAINTS"],"prefix":"10.1142","volume":"10","author":[{"given":"ORTRUN","family":"IBENS","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MARC","family":"FUCHS","sequence":"additional","affiliation":[{"name":"sd&amp;m Software Design &amp; Management AG, M\u00fcnchen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2012,4,30]]},"reference":[{"key":"p_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881947"},{"key":"p_5","doi-asserted-by":"publisher","DOI":"10.1007\/BF00244282"},{"key":"p_8","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005808119103"},{"key":"p_10","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(85)90012-8"},{"key":"p_11","doi-asserted-by":"publisher","DOI":"10.1007\/BF00297245"},{"key":"p_12","first-page":"135","volume":"4","author":"Robinson G. A.","year":"1969","journal-title":"Machine Intelligence"},{"key":"p_13","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1131"},{"key":"p_14","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90004-2"},{"key":"p_16","doi-asserted-by":"publisher","DOI":"10.1137\/0204036"},{"key":"p_17","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005839515219"},{"issue":"2","key":"p_20","first-page":"113","volume":"10","author":"Markovitch S.","year":"1993","journal-title":"Information Filtering: Selection Mechanisms in Learning Systems. Machine Learning"},{"key":"p_23","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(90)90059-9"},{"key":"p_24","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.3.217"}],"container-title":["International Journal on Artificial Intelligence Tools"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218213001000477","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T13:52:18Z","timestamp":1565185938000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218213001000477"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,3]]},"references-count":13,"journal-issue":{"issue":"01n02","published-online":{"date-parts":[[2012,4,30]]},"published-print":{"date-parts":[[2001,3]]}},"alternative-id":["10.1142\/S0218213001000477"],"URL":"https:\/\/doi.org\/10.1142\/s0218213001000477","relation":{},"ISSN":["0218-2130","1793-6349"],"issn-type":[{"value":"0218-2130","type":"print"},{"value":"1793-6349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,3]]}}}