{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:37:55Z","timestamp":1725471475834},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540659228"},{"type":"electronic","value":"9783540488552"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/10703163_24","type":"book-chapter","created":{"date-parts":[[2006,10,9]],"date-time":"2006-10-09T18:15:50Z","timestamp":1160417750000},"page":"355-371","source":"Crossref","is-referenced-by-count":3,"title":["On the Complexity of H-Subsumption"],"prefix":"10.1007","author":[{"given":"Reinhard","family":"Pichler","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"24_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based Equational Theorem Proving with Selection and Simplification. Journal of Logic and Computation\u00a04(3), 217\u2013247 (1994)","journal-title":"Journal of Logic and Computation"},{"key":"24_CR2","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"F. Baader","year":"1994","unstructured":"Baader, F., Siekmann, J.H.: Unification Theory. In: Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford University Press, Oxford (1994)"},{"key":"24_CR3","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"Comon, H., Lescanne, P.: Equational Problems and Disunification. Journal of Symbolic Computation\u00a07, 371\u2013425 (1989)","journal-title":"Journal of Symbolic Computation"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/3-540-61377-3_35","volume-title":"Computer Science Logic","author":"R. Caferra","year":"1996","unstructured":"Caferra, R., Peltier, N.: Decision Procedures using Model Building Techniques. In: Kleine B\u00fcning, H. (ed.) CSL 1995. LNCS, vol.\u00a01092, pp. 130\u2013144. Springer, Heidelberg (1996)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BFb0018439","volume-title":"Logics in AI","author":"R. Caferra","year":"1991","unstructured":"Caferra, R., Zabel, N.: Extending Resolution for Model Construction. In: van Eijck, J. (ed.) JELIA 1990. LNCS, vol.\u00a0478, pp. 153\u2013169. Springer, Heidelberg (1991)"},{"issue":"2","key":"24_CR6","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C. Ferm\u00fcller","year":"1996","unstructured":"Ferm\u00fcller, C., Leitsch, A.: Hyperresolution and Automated Model Building. Journal of Logic and Computation\u00a06(2), 173\u2013230 (1996)","journal-title":"Journal of Logic and Computation"},{"key":"24_CR7","volume-title":"Computers and Intractability, A guide to the Theory of NP-Completeness","author":"M.R. Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability, A guide to the Theory of NP-Completeness. W.H. Freeman and Company, New York (1979)"},{"issue":"3","key":"24_CR8","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"Hsiang, J., Rusinowitch, M.: Proving Refutational Completeness of Theorem- Proving Strategies: The Transfinite Semantic Tree Method. Journal of the ACM\u00a038(3), 559\u2013587 (1991)","journal-title":"Journal of the ACM"},{"key":"24_CR9","first-page":"87","volume":"4","author":"R. Kowalski","year":"1969","unstructured":"Kowalski, R., Hayes, P.J.: Semantic Trees in Automated Theorem Proving. Machine Intelligence\u00a04, 87\u2013101 (1969)","journal-title":"Machine Intelligence"},{"key":"24_CR10","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60605-2","volume-title":"The Resolution Calculus","author":"A. Leitsch","year":"1997","unstructured":"Leitsch, A.: The Resolution Calculus. Texts in Theoretical Computer Science. Springer, Heidelberg (1997)"},{"key":"24_CR11","first-page":"1","volume":"11","author":"R. Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R., Rubio, A.: Theorem Proving with ordering and equality constrained clauses. Journal of Symbolic Computation\u00a011, 1\u201332 (1995)","journal-title":"Journal of Symbolic Computation"},{"key":"24_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/3-540-49545-2_14","volume-title":"Logics in Artificial Intelligence","author":"R. Pichler","year":"1998","unstructured":"Pichler, R.: Algorithms on atomic representations of herbrand models. In: Dix, J., Fari\u00f1as del Cerro, L., Furbach, U. (eds.) JELIA 1998. LNCS (LNAI), vol.\u00a01489, pp. 199\u2013215. Springer, Heidelberg (1998)"},{"key":"24_CR13","series-title":"Lecture Notes in Artificial Intelligence","first-page":"193","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"R. Pichler","year":"1998","unstructured":"Pichler, R.: Completeness and redundancy in constrained clause logic. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol.\u00a01761, pp. 193\u2013203. Springer, Heidelberg (1998), \n                    \n                      http:\/\/www.logic.at\/ftp98"},{"key":"24_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"L.J. Stockmeyer","year":"1976","unstructured":"Stockmeyer, L.J.: The Polynomial Time Hierarchy. Journal of Theoretical Computer Science\u00a03, 1\u201312 (1976)","journal-title":"Journal of Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10703163_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T07:55:27Z","timestamp":1552636527000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10703163_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540659228","9783540488552"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/10703163_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}