{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T18:02:36Z","timestamp":1648922556291},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2004,12,31]],"date-time":"2004-12-31T00:00:00Z","timestamp":1104451200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2005,1]]},"DOI":"10.1007\/s10472-005-0434-4","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T19:19:42Z","timestamp":1109791182000},"page":"255-294","source":"Crossref","is-referenced-by-count":1,"title":["On deciding subsumption problems"],"prefix":"10.1007","volume":"43","author":[{"given":"Uwe","family":"Egly","sequence":"first","affiliation":[]},{"given":"Reinhard","family":"Pichler","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Woltran","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,12,31]]},"reference":[{"key":"434_CR1","unstructured":"F. Baader and J.H. Siekmann, Unification theory, in: Handbook of Logic in Artificial Intelligence and Logic Programming, eds. D.M. Gabbay, C.J. Hogger and J.A. Robinson (1994) pp. 41\u2013125."},{"key":"434_CR2","unstructured":"M. Cadoli, A. Giovanardi and M. Schaerf, An algorithm to evaluate quantified Boolean formulae, in: Proceedings of the 15th National Conference on Artificial Intelligence (AAAI\u201998) (1998) pp. 262-267."},{"key":"434_CR3","doi-asserted-by":"crossref","unstructured":"R. Caferra and N. Peltier, Decision procedures using model building techniques, in: Proceedings of the 9th International Workshop for Computer Science Logic (CSL\u201995), ed. H. Kleine B\u00fcning, Lecture Notes in Computer Science, Vol. 1092 (1996) pp. 130\u2013144.","DOI":"10.1007\/3-540-61377-3_35"},{"key":"434_CR4","doi-asserted-by":"crossref","unstructured":"R. Caferra and N. Zabel, Extending resolution for model construction, in: Logics in Artificial Intelligence (JELIA\u201990), Proceedings, ed. J. van Eijck, Lecture Notes in Computer Science, Vol. 478 (1991) pp. 153\u2013169.","DOI":"10.1007\/BFb0018439"},{"key":"434_CR5","unstructured":"A. Colmerauer, Equations and inequations on finite and infinite trees, in: Proceedings of the International Conference on Fifth Generation Computer Systems (FGCS\u201984) (1984) pp. 85\u201399."},{"issue":"2","key":"434_CR6","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1006\/inco.1994.1056","volume":"112","author":"H. Comon","year":"1994","unstructured":"H. Comon and C. Delor, Equational formulae with membership constraints, Information and Computation 112(2) (1994) 167\u2013216.","journal-title":"Information and Computation"},{"issue":"3\u20134","key":"434_CR7","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"H. Comon and P. Lescanne, Equational problems and disunification, Journal of Symbolic Computation 7(3\u20134) (1989) 371\u2013425.","journal-title":"Journal of Symbolic Computation"},{"key":"434_CR8","doi-asserted-by":"crossref","unstructured":"J. Delgrande, T. Schaub, H. Tompits and S. Woltran, On computing solutions to belief change scenarios, in: Proceedings of the 6th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU\u201901), eds. S. Benferhat and P. Besnard, Lecture Notes in Computer Science, Vol. 2143 (2001) pp. 510\u2013521.","DOI":"10.1007\/3-540-44652-4_45"},{"key":"434_CR9","unstructured":"U. Egly, T. Eiter, H. Tompits and S. Woltran, Solving advanced reasoning tasks using quantified Boolean formulas, in: Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI\u201900) (2000) pp. 417\u2013422."},{"key":"434_CR10","unstructured":"U. Egly, H. Tompits and S. Woltran, On quantifier shifting for quantified Boolean formulas, in: Proceedings of the SAT-02 Workshop on Theory and Applications of Quantified Boolean Formulas (QBF-02) (2002) pp. 48\u201361."},{"key":"434_CR11","unstructured":"R. Feldmann, B. Monien and S. Schamberger, A distributed algorithm to evaluate quantified Boolean formulas, in: Proceedings of the 17th National Conference on Artificial Intelligence (AAAI\u201900) (2000) pp. 285\u2013290."},{"issue":"2","key":"434_CR12","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C. Ferm\u00fcller","year":"1996","unstructured":"C. Ferm\u00fcller and A. Leitsch, Hyperresolution and automated model building, Journal of Logic and Computation 6(2) (1996) 173\u2013203.","journal-title":"Journal of Logic and Computation"},{"key":"434_CR13","unstructured":"M.R. Garey and D.S. Johnson, Computers and Intractability, A Guide to the Theory of NP-Completeness (Freeman, 1979)."},{"key":"434_CR14","doi-asserted-by":"crossref","unstructured":"E. Giunchiglia, M. Narizzano and A. Tacchella, QuBE: A system for deciding quantified Boolean formulas satisfiability, in: Proceedings of the International Joint Conference on Automated Reasoning (IJCAR\u201901) eds. R. Gor\u00e9, A. Leitsch and T. Nipkow (2001) pp. 364\u2013369.","DOI":"10.1007\/3-540-45744-5_27"},{"key":"434_CR15","doi-asserted-by":"crossref","unstructured":"E. Goldberg and Y. Novikov, BerkMin: A fast and robust sat-solver, in: Proceedings of the Design, Automation and Test in Europe Conference (DATE\u201902) (2002) pp. 142\u2013149.","DOI":"10.1109\/DATE.2002.998262"},{"issue":"1\u20132","key":"434_CR16","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/0304-3975(95)00207-3","volume":"166","author":"G. Gottlob","year":"1996","unstructured":"G. Gottlob, S. Marcus, A. Nerode, G. Salzer and V.S. Subrahmanian, A non-ground realization of the stable and well-founded semantics, Theoretical Computer Science 166(1\u20132) (1996) 221\u2013262.","journal-title":"Theoretical Computer Science"},{"key":"434_CR17","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1006\/inco.2000.2915","volume":"165","author":"G. Gottlob","year":"2001","unstructured":"G. Gottlob and R. Pichler, Working with ARMs: Complexity results on atomic representations of Herbrand models, Information and Computation 165 (2001) 183\u2013207.","journal-title":"Information and Computation"},{"issue":"4","key":"434_CR18","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BF01893885","volume":"28","author":"D. Kapur","year":"1991","unstructured":"D. Kapur, P. Narendran, D. Rosenkrantz and H. Zhang, Sufficient-completeness, ground-reducibility and their complexity, Acta Informatica 28(4) (1991) 311\u2013350.","journal-title":"Acta Informatica"},{"key":"434_CR19","unstructured":"H. Kautz and B. Selman, Planning as satisfiability, in: Proceedings of the 10th European Conference on Artificial Intelligence (ECAI\u201992), ed. B. Neumann (1992) pp. 359\u2013363."},{"issue":"1","key":"434_CR20","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine B\u00fcning","year":"1995","unstructured":"H. Kleine B\u00fcning, M. Karpinski and A. Fl\u00f6gel, Resolution for quantified Boolean formulas, Information and Computation 117(1) (1995) 12\u201318.","journal-title":"Information and Computation"},{"key":"434_CR21","unstructured":"K. Kunen, Answer sets and negation as failure, in: Proceedings of the 4th International Conference on Logic Programming (ICLP\u201987), ed. J.-L. Lassez (1987) pp. 219\u2013228."},{"key":"434_CR22","doi-asserted-by":"crossref","unstructured":"G. Kuper, K. McAloon, K. Palem and K. Perry, Efficient parallel algorithms for anti-unification and relative complement, in: Proceedings of the 3rd Annual Symposium on Logic in Computer Science (LICS\u201988) (1988) pp. 112\u2013120.","DOI":"10.1109\/LICS.1988.5109"},{"key":"434_CR23","unstructured":"J.-L. Lassez, M. Maher and K. Marriott, Unification revisited, in: Foundations of Logic and Functional Programming, Proceedings (1986) pp. 67\u2013113."},{"key":"434_CR24","doi-asserted-by":"crossref","unstructured":"J.-L. Lassez, M. Maher and K. Marriott, Elimination of negation in term algebras, in: Proceedings of the 16th International Symposium on Mathematical Foundations of Computer Science (MFCS\u201991), ed. A. Tarlecki (1991) pp. 1\u201316.","DOI":"10.1007\/3-540-54345-7_44"},{"issue":"3","key":"434_CR25","first-page":"301","volume":"3","author":"J.-L. Lassez","year":"1987","unstructured":"J.-L. Lassez and K. Marriott, Explicit representation of terms defined by counter examples, Journal of Automated Reasoning 3(3) (1987) 301\u2013317.","journal-title":"Journal of Automated Reasoning"},{"key":"434_CR26","doi-asserted-by":"crossref","unstructured":"R. Letz, Lemma and model caching in decision procedures for quantified Boolean formulas, in: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2002, eds. U. Egly and C.G. Ferm\u00fcller, Lecture Notes in Computer Science, Vol. 2381 (2002) pp. 160\u2013175.","DOI":"10.1007\/3-540-45616-3_12"},{"issue":"2","key":"434_CR27","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari, An efficient unification algorithm, ACM Transactions on Programming Languages and Systems 4(2) (1982) 258\u2013282.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"434_CR28","doi-asserted-by":"crossref","unstructured":"M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang and S. Malik, Chaff: Engineering an efficient SAT solve, in: Proceedings of the 38th Design Automation Conference (DAC\u201901) (2001).","DOI":"10.1145\/378239.379017"},{"key":"434_CR29","unstructured":"C.H. Papadimitriou, Computational Complexity (Addison-Wesley, 1994)."},{"key":"434_CR30","doi-asserted-by":"crossref","unstructured":"D. Pearce, H. Tompits and S. Woltran, Encodings for equilibrium logic and logic programs with nested expressions, in: Progress in Artificial Intelligence, Knowledge Extraction, Multi-agent Systems, Logic Programming and Constraint Solving, 10th Portuguese Conference on Artificial Intelligence (EPIA\u201901), eds. P. Brazdil and A. Jorge, Lecture Notes in Computer Science, Vol. 2258 (2001) pp. 306\u2013320.","DOI":"10.1007\/3-540-45329-6_31"},{"key":"434_CR31","unstructured":"R. Pichler, On the complexity of H-subsumption, in: Proceedings of the 12th International Workshop for Computer Science Logic (CSL\u201998), eds. G. Gottlob, E. Grandjean and K. Seyr, Lecture Notes in Computer Science, Vol. 1584 (1998) pp. 355\u2013371."},{"key":"434_CR32","doi-asserted-by":"crossref","unstructured":"R. Pichler, Completeness and redundancy in constrained clause logic, in: Automated Deduction in Classical and Non-Classical Logics, Selected Papers, eds. R. Caferra and G. Salzer, Lecture Notes in Computer Science, Vol. 1761 (2000) pp. 221\u2013235.","DOI":"10.1007\/3-540-46508-1_15"},{"key":"434_CR33","doi-asserted-by":"crossref","unstructured":"R. Pichler, The explicit representability of implicit generalizations, in: Proceedings of the 11th International Conference on Rewriting Techniques and Applications (RTA\u201900), ed. L. Bachmair (2000) pp. 187\u2013202.","DOI":"10.1007\/10721975_13"},{"issue":"3","key":"434_CR34","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"D.A. Plaisted and S. Greenbaum, A structure preserving clause form translation, Journal of Symbolic Computation 2(3) (1986) 293\u2013304.","journal-title":"Journal of Symbolic Computation"},{"key":"434_CR35","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","volume":"10","author":"J. Rintanen","year":"1999","unstructured":"J. Rintanen, Constructing conditional plans by a theorem prover, Journal of Artificial Intelligence Research 10 (1999) 323\u2013352.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"434_CR36","unstructured":"J. Rintanen, Improvements to the evaluation of quantified Boolean formulae, in: Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI\u201999), ed. T. Dean (1999) pp. 1192\u20131197."},{"key":"434_CR37","volume-title":"Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970","author":"J. Siekmann","year":"1983","unstructured":"J. Siekmann and G. Wrightson, eds., Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970, Vol. 2 (Springer, Berlin, 1983)."},{"key":"434_CR38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"L. Stockmeyer","year":"1977","unstructured":"L. Stockmeyer, The polynomial-time hierarchy, Theoretical Computer Science 3 (1977) 1\u201322.","journal-title":"Theoretical Computer Science"},{"key":"434_CR39","doi-asserted-by":"crossref","unstructured":"G. Tseitin, On the complexity of proofs in propositional logics, Seminars in Mathematics 8 (1970), reprinted in [37].","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"434_CR40","doi-asserted-by":"crossref","unstructured":"H. Zhang, SATO: An efficient propositional prover, in: Proceedings of the 17th Internationonal Conference on Automated Deduction (CADE-17), ed. W. McCune (1997) pp. 272-275.","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-005-0434-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-005-0434-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-005-0434-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T02:26:43Z","timestamp":1586140003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-005-0434-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,12,31]]},"references-count":40,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["434"],"URL":"https:\/\/doi.org\/10.1007\/s10472-005-0434-4","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,12,31]]}}}