{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:48:00Z","timestamp":1767926880337,"version":"3.49.0"},"reference-count":59,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50029-1","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T09:04:11Z","timestamp":1181552651000},"page":"1965-2013","source":"Crossref","is-referenced-by-count":97,"title":["Combining Superposition, Sorts and Splitting"],"prefix":"10.1016","author":[{"given":"Christoph","family":"Weidenbach","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50029-1_bb0005","series-title":"Proceedings of 8th International Joint Conference on Artificial Intelligence, IJCAI-83","first-page":"916","article-title":"Terminator","author":"Antoniou","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0010","series-title":"Term Rewriting and All That","author":"Baader","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0015","first-page":"445","article-title":"Unification theory","volume":"Vol. I","author":"Baader","year":"2001"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50029-1_bb0020","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","article-title":"Rewrite-based equational theorem proving with selection and simplification","volume":"4","author":"Bachmair","year":"1994","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0025","first-page":"19","article-title":"Resolution theorem proving","volume":"Vol. I","author":"Bachmair","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0030","series-title":"Computational Logic and Proof Theory, Third Kurt G\u00f6del Colloquium","first-page":"83","article-title":"Superposition with simplification as a decision procedure for the monadic class with equality","author":"Bachmair","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0035","series-title":"Proceedings of the 10th International Conference on Automated Deduction","first-page":"442","article-title":"Simultaneous paramodulation","author":"Benanav","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0040","series-title":"Computer Science and Applied Mathematics","article-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","year":"1973"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0045","series-title":"Proceedings 13th IEEE Symposium on Logic in Computer Science, LICS'98","first-page":"58","article-title":"The horn mu-calculus","author":"Charatonik","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0050","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/BF00156916","article-title":"Are tableaux an improvement on truth-tables?","volume":"1","author":"D'Agostino","year":"1992","journal-title":"Journal of Logic, Language and Information"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0055","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","article-title":"Orderings for term-rewriting systems","volume":"17","author":"Dershowitz","year":"1982","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50029-1_bb0060","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","article-title":"Termination of rewriting","volume":"3","author":"Dershowitz","year":"1987","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0065","first-page":"533","article-title":"Rewriting","volume":"Vol. I","author":"Dershowitz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0070","first-page":"1009","article-title":"Higher-order unification and matching","volume":"Vol. II","author":"Dowek","year":"2001"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50029-1_bb0075","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","article-title":"Linear-time algorithms for testing the satisfiability of propositional horn formulae","volume":"1","author":"Dowling","year":"1984","journal-title":"Journal of Logic Programming"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50029-1_bb0080","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1145\/322217.322228","article-title":"Variations on the common subexpression problem","volume":"27","author":"Downey","year":"1980","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0085","article-title":"Completeness, Confluence, and Related Properties of Clause Graph Resolution","author":"Eisinger","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0090","series-title":"Automated Deduction \u2212 A Basis for Applications","first-page":"265","article-title":"Deduction-based software component retrieval","author":"Fischer","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0095","series-title":"Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, LICS'91","first-page":"300","article-title":"Logic programs as types for logic programs","author":"Fr\u00fchwirth","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0100","series-title":"Proceedings of the 14th International Conference on Automated Deduction, CADE-14","first-page":"321","article-title":"Soft typing for ordered resolution","author":"Ganzinger","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0105","article-title":"Computers and intractability: A guide to the theory of NP-completeness","author":"Garey","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0110","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0004-3702(93)90069-N","article-title":"Removing redundancy from a clause","volume":"61","author":"Gottlob","year":"1993","journal-title":"Artificial Intelligence"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50029-1_bb0115","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1145\/3149.214118","article-title":"On the efficiency of subsumption algorithms","volume":"32","author":"Gottlob","year":"1985","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0120","first-page":"100","article-title":"Tableaux and related methods","volume":"Vol. I","author":"H\u00e4hnle","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0125","series-title":"Workshop on Formal Methods and Security Protocols","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0130","series-title":"16th International Conference on Automated Deduction, CADE-16","first-page":"232","article-title":"Waldmeister \u2013 improvements in performance and ease of use","author":"Hillenbrand","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0135","series-title":"Proceedings of 15th International Joint Conference on Artificial Intelligence, IJCAI-97","first-page":"202","article-title":"On evaluating decision procedures for model logics","author":"Hustadt","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0140","series-title":"Rewriting Techniques and Applications, 9th International Conference, RTA-98","first-page":"76","article-title":"Unification in extensions of shallow equational theories","author":"Jacquemard","year":"1998"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50029-1_bb0145","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1145\/321958.321960","article-title":"Resolution strategies as decision procedures","volume":"23","author":"Joyner","year":"1976","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0150","series-title":"Proceedings of the 13th National Conference on AI, AAAI'96","first-page":"1194","article-title":"Pushing the envelope: Planning, propositional logic and stochastic search","author":"Kautz","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0155","series-title":"Computational Problems in Abstract Algebra","first-page":"263","article-title":"Simple word problems in universal algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0160","series-title":"11th International Conference on Automated Deduction, CADE-11","first-page":"209","article-title":"Experiments in automated deduction with condensed detachment","author":"McCune","year":"1992"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50029-1_bb0165","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1023\/A:1005843632307","article-title":"Otter","volume":"18","author":"McCune","year":"1997","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0170","article-title":"Soft Typing for Clausal Inference Systems","author":"Meyer","year":"1999","journal-title":"Dissertation, Technische Fakult\u00e4t der Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0175","series-title":"Proceedings 11th IEEE Symposium on Logic in Computer Science, LICS'96","first-page":"473","article-title":"Basic paramodulation and decidable theories (extended abstract)","author":"Nieuwenhuis","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0180","first-page":"371","article-title":"Paramodulation-based theorem proving","volume":"Vol. I","author":"Nieuwenhuis","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0185","series-title":"Rewriting Techniques and Applications, 5th International Conference, RTA-93","first-page":"436","article-title":"Saturation of first-order (constrained) clauses with the Saturate system","author":"Nivela","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0190","series-title":"15th International Conference on Automated Deduction, CADE-15","first-page":"397","article-title":"On generating small clause normal forms","author":"Nonnengart","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0195","first-page":"335","article-title":"Computing small clause normal forms","volume":"Vol. I","author":"Nonnengart","year":"2001"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50029-1_bb0200","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","article-title":"A technique for establishing completeness results in theorem proving with equality","volume":"12","author":"Peterson","year":"1983","journal-title":"SIAM Journal of Computation"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0205","first-page":"1853","article-title":"Term indexing","volume":"Vol. II","author":"Ramakrishnan","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0210","series-title":"16th International Conference on Automated Deduction, CADE-16","first-page":"292","article-title":"Vampire","author":"Riazanov","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0215","series-title":"Limited resource strategy in resolution theorem proving","author":"Riazanov","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0220","series-title":"Splitting without backtracking","author":"Riazanov","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0225","series-title":"Machine Intelligence 4","first-page":"135","article-title":"Paramodulation and theorem-proving in first-order theories with equality","author":"Robinson","year":"1969"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50029-1_bb0230","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0235","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0304-3975(88)90146-6","article-title":"Implication of clauses is undecidable","volume":"59","author":"Schmidt-Schauss","year":"1988","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0240","series-title":"16th International Conference on Automated Deduction, CADE-16","first-page":"297","article-title":"System abstract: E 0.3","author":"Schulz","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0245","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0020-0190(93)90105-I","article-title":"On the complexity of recursive path orderings","volume":"46","author":"Snyder","year":"1993","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0250","series-title":"9th International Conference on Automated Deduction, CADE-9","first-page":"573","article-title":"A subsumption algorithm based on characteristic matrices","author":"Socher","year":"1988"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50029-1_bb0255","doi-asserted-by":"crossref","first-page":"648","DOI":"10.1145\/321784.321792","article-title":"The concept of weak substitution in theorem-proving","volume":"20","author":"Stillman","year":"1973","journal-title":"Journal of the ACM"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50029-1_bb0260","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1023\/A:1005806324129","article-title":"The tptp problem library \u2013 cnf release v1.2.1","volume":"21","author":"Sutcliffe","year":"1998","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50029-1_bb0265","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1006285423991","article-title":"The cade-15 atp system competition","volume":"23","author":"Sutcliffe","year":"1999","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0270","series-title":"15th International Conference on Automated Deduction, CADE-15","first-page":"427","article-title":"Towards efficient subsumption","author":"Tammet","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0275","article-title":"Computational Aspects of a First-Order Logic with Sorts","author":"Weidenbach","year":"1996","journal-title":"Dissertation, Technische Fakult\u00e4t der Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0280","series-title":"Automated Deduction \u2013 A Basis for Applications","first-page":"291","article-title":"Sorted unification and tree automata","author":"Weidenbach","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0285","series-title":"16th International Conference on Automated Deduction, CADE-16","first-page":"378","article-title":"Towards an automatic analysis of security protocols in first-order logic","author":"Weidenbach","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50029-1_bb0290","series-title":"16th International Conference on Automated Deduction, CADE-16","first-page":"314","article-title":"System description: Spass version 1.0.0","author":"Weidenbach","year":"1999"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50029-1_bb0295","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","article-title":"Efficiency and completeness of the set of support strategy in theorem proving","volume":"12","author":"Wos","year":"1965","journal-title":"Journal of the ACM"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500291?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500291?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,6]],"date-time":"2019-01-06T14:25:39Z","timestamp":1546784739000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500291"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":59,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50029-1","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}