{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2021,5,11]],"date-time":"2021-05-11T19:12:57Z","timestamp":1620760377686},"reference-count":12,"publisher":"Association for Computing Machinery (ACM)","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[1985,4]]},"abstract":"\n The costs of subsumption algorithms are analyzed by an estimation of the maximal number of unification attempts (worst-case unification complexity) made for deciding whether a clause\n C<\/jats:italic>\n subsumes a clause\n D<\/jats:italic>\n . For this purpose the clauses\n C<\/jats:italic>\n and\n D<\/jats:italic>\n are characterized by the following parameters: number of variables in\n C<\/jats:italic>\n , number of literals in\n C<\/jats:italic>\n , number of literals in\n D<\/jats:italic>\n , and maximal length of the literals. The worst-case unification complexity immediately yields a lower bound for the worst-case time complexity.\n <\/jats:p>\n \n First, two well-known algorithms (Chang-Lee, Stillman) are investigated. Both algorithms are shown to have a very high worst-case time complexity. Then, a new subsumption algorithm is defined, which is based on an analysis of the connection between variables and predicates in\n C<\/jats:italic>\n . An upper bound for the worst-case unification complexity of this algorithm, which is much lower than the lower bounds for the two other algorithms, is derived. Examples in which exponential costs are reduced to polynomial costs are discussed. Finally, the asymptotic growth of the worst-case complexity for all discussed algorithms is shown in a table (for several combinations of the parameters).\n <\/jats:p>","DOI":"10.1145\/3149.214118","type":"journal-article","created":{"date-parts":[[2002,7,27]],"date-time":"2002-07-27T11:25:57Z","timestamp":1027769157000},"page":"280-295","source":"Crossref","is-referenced-by-count":42,"title":["On the efficiency of subsumption algorithms"],"prefix":"10.1145","volume":"32","author":[{"given":"G.","family":"Gottlob","sequence":"first","affiliation":[{"name":"Politecnico di Milano, Dipartimento di Elettronica, 20133, Milano-Piazza Leonardo Da Vinci, 32, Italy and Technische Universit\u00e4t Wien, Vienna, Austria"}]},{"given":"A.","family":"Leitsch","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Statistik und Mathematik, Wirtschaftsuniversit\u00e4t Wien, Augasse 2-6, 1090 Vienna, Austria"}]}],"member":"320","reference":[{"key":"e_1_2_1_1_2","first-page":"511","volume-title":"Proceedings of the IJCAI-81","author":"BL~ SIUS","year":"1981"},{"key":"e_1_2_1_2_2","unstructured":"CHANG C.L. AND LEE R. C. T.Symbolic Logic and Mechanical Theorem Proving. Academic Press New York i 973. CHANG C.L. AND LEE R. C. T.Symbolic Logic and Mechanical Theorem Proving. Academic Press New York i 973."},{"key":"e_1_2_1_3_2","first-page":"480","volume-title":"Proceedings of the IJCAI-81 (Vancouver","author":"EISINGER N.","year":"1981"},{"key":"e_1_2_1_4_2","volume-title":"Computers and intractability","year":"1979"},{"key":"e_1_2_1_5_2","first-page":"45","volume-title":"Proceedings of the Austrian Academy of Sciences, II","volume":"192","author":"LEITSCH A.","year":"1983"},{"key":"e_1_2_1_6_2","unstructured":"Loveland D. Automated Theorm Proving: A Lt~ irnl Ratio Nltwth.l-lnlland Amsterdam 1978 Loveland D. Automated Theorm Proving: A Lt~ irnl Ratio Nltwth.l-lnlland Amsterdam 1978"},{"key":"e_1_2_1_7_2","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"8","author":"MCCHAREN J.D.","year":"1976","journal-title":"IEEE Trans. Comput. C-25"},{"key":"e_1_2_1_8_2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"PATERSON M.S.","year":"1978","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_2_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/321784.321792"},{"key":"e_1_2_1_11_2","doi-asserted-by":"crossref","first-page":"782","DOI":"10.1109\/TC.1976.1674697","volume":"8","author":"WILSON G.A.","year":"1976","journal-title":"IEEE Trans. Comput. C-25"},{"key":"e_1_2_1_12_2","first-page":"867","volume-title":"Proceedings of the 8th IJCAI- 83","volume":"2","year":"1983"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3149.214118","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,2]],"date-time":"2021-03-02T14:29:03Z","timestamp":1614695343000},"score":1,"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985,4]]},"references-count":12,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1985,4]]}},"alternative-id":["10.1145\/3149.214118"],"URL":"http:\/\/dx.doi.org\/10.1145\/3149.214118","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":["Artificial Intelligence","Hardware and Architecture","Information Systems","Control and Systems Engineering","Software"],"published":{"date-parts":[[1985,4]]}}}