{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:58:10Z","timestamp":1779087490575,"version":"3.51.4"},"reference-count":60,"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\/50004-7","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"19-99","source":"Crossref","is-referenced-by-count":225,"title":["Resolution Theorem Proving"],"prefix":"10.1016","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Ganzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"McAllester","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christopher","family":"Lynch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/B978-044450813-3\/50004-7_bb0010","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BF00881838","article-title":"Gentzen-type systems, resolution and tableaux","volume":"10","author":"Avron","year":"1993","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0015","first-page":"273","article-title":"Normal form transformations","volume":"Vol. I","author":"Baaz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0020","series-title":"Proc. EUROCAL 87","first-page":"452","article-title":"Critical pair criteria for rewriting modulo a congruence","author":"Bachmair","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0025","series-title":"Proc. 10th Int. Conf. on Automated Deduction","first-page":"427","article-title":"On restrictions of ordered paramodulation with simplification","author":"Bachmair","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50004-7_rf0030","series-title":"Proc. 9th IEEE Symposium on Logic in Computer Science","first-page":"384","article-title":"Rewrite techniques for transitive relations","author":"Bachmair","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0035","series-title":"Proc. of Third Kurt G\u00f6del Colloquium, KGC'93","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\/50004-7_bb0040","series-title":"Proc. 11th IEEE Symposium on Logic in Computer Science","first-page":"456","article-title":"Complexity analysis based on ordered resolution","author":"Basin","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0045","series-title":"Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR'92)","first-page":"119","article-title":"An ordered theory resolution calculus","author":"Baumgartner","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0050","article-title":"Locking: A restriction of resolution","author":"Boyer","year":"1971","journal-title":"PhD thesis, University of Texas at Austin, Austin, TX"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0055","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","article-title":"Proving theorems with the modification method","volume":"4","author":"Brand","year":"1975","journal-title":"SIAM J. Comput."},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0060","series-title":"Conditional Term Rewriting Systems, Third International Workshop","first-page":"242","article-title":"Reduction techniques for first-order reasoning","volume":"656","author":"Bronsard","year":"1992"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50004-7_bb0065","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","article-title":"Symbolic boolean manipulation with ordered binary-decision diagrams","volume":"24","author":"Bryant","year":"1992","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0070","series-title":"Proc. 10th CADE","first-page":"178","article-title":"A resolution principle for clauses with constraints","author":"B\u00fcrckert","year":"1990"},{"issue":"7","key":"10.1016\/B978-044450813-3\/50004-7_bb0075","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem proving","volume":"5","author":"Davis","year":"1962","journal-title":"Communications ACM"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0080","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","article-title":"A computing procedure for quantification theory","volume":"7","author":"Davis","year":"1960","journal-title":"J. Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0085","article-title":"Ordering refinements of resolution","author":"de Nivelle","year":"1996","journal-title":"PhD thesis, Technische Universiteit Delft"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0090","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":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0095","series-title":"Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning (LPAR'93)","first-page":"122","article-title":"Ordered paramodulation and resolution as decision procedure","author":"Ferm\u00fcller","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0100","first-page":"1791","article-title":"Resolution decision procedures","volume":"Vol. II","author":"Ferm\u00fcller","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0105","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-56732-1","article-title":"Resolution Methods for the Decision Problem","author":"Ferm\u00fcller","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0110","series-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"Gallier","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0115","series-title":"Automated Deduction \u2014 CADE'14","first-page":"321","article-title":"Soft typing for ordered resolution","author":"Ganzinger","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0120","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1147\/rd.41.0028","article-title":"A proof method for quantification theory","volume":"4","author":"Gilmore","year":"1960","journal-title":"IBM J. Res. Develop."},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0125","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","article-title":"Refutational theorem proving using term-rewriting systems","volume":"25","author":"Hsiang","year":"1985","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0130","article-title":"Constrained Resolution: A Complete Method for Higher Order Logic","author":"Huet","year":"1972","journal-title":"PhD thesis, Case Western Reserve University"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0135","article-title":"Resolution-Based Decisison Procedures for Subclasses of First-Order Logic","author":"Hustadt","year":"1999","journal-title":"PhD thesis, Fachbereich Informatik, Universit\u00e4t des Saarlandes, Germany"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50004-7_rf0140","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":"J. Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0145","series-title":"Proc. Ninth International Joint Conference on Artificial Intelligence","first-page":"1146","article-title":"An equational approach to theorem proving in first-order predicate calculus","author":"Kapur","year":"1985"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50004-7_bb0150","first-page":"9","article-title":"Deduction with symbolic constraints","volume":"4","author":"Kirchner","year":"1990","journal-title":"Revue Francaise d'Intelligence Artificielle"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0155","series-title":"Twelfth International Conference on Automated Deduction","first-page":"708","article-title":"Semantic tableaux with ordering restrictions","author":"Klingenbeck","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0160","series-title":"Proceedings of the IFIP Congress","first-page":"569","article-title":"Predicate logic as programming language","author":"Kowalski","year":"1974"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0165","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","article-title":"Linear resolution with selection function","volume":"2","author":"Kowalski","year":"1971","journal-title":"Artificial Intelligence"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50004-7_bb0170","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00245018","article-title":"What is the inverse method?","volume":"5","author":"Lifschitz","year":"1989","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0175","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","article-title":"A simplified format for the model-elimination theorem-proving procedure","volume":"16","author":"Loveland","year":"1969","journal-title":"J. Association for Computing Machinery"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50004-7_bb0180","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1006\/jsco.1996.0075","article-title":"Oriented equational logic is complete","volume":"23","author":"Lynch","year":"1997","journal-title":"J. Symbolic Computation"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50004-7_bb0185","doi-asserted-by":"crossref","DOI":"10.1145\/357084.357090","article-title":"A deductive approach to program synthesis","volume":"2","author":"Manna","year":"1980","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0190","first-page":"1420","article-title":"An inverse method for establishing deducibility in the classical predicate calculus","volume":"159","author":"Maslov","year":"1964","journal-title":"Dokl. Akad. Nauk SSSR"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50004-7_bb0195","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1145\/151261.151265","article-title":"Automated recognition of tractability in inference relations","volume":"40","author":"McAllester","year":"1993","journal-title":"J. Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0200","article-title":"Topics in completion theorem proving","author":"M\u00fcller","year":"1988","journal-title":"Research Report Memo SEKI-SR-88-13, Univ. Kaiserslautern"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50004-7_bb0205","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0004-3702(82)90011-X","article-title":"Completely non-clausal theorem proving","volume":"18","author":"Murray","year":"1982","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0210","series-title":"Automated Deduction \u2014 CADE'11","first-page":"477","article-title":"Theorem proving with ordering constrained clauses","author":"Nieuwenhuis","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0215","series-title":"Proc. 12th International Conference on Automated Deduction","first-page":"545","article-title":"AC-superposition with constraints: No AC-unifiers needed","author":"Nieuwenhuis","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0220","first-page":"371","article-title":"Paramodulation-based theorem proving","volume":"Vol. I","author":"Nieuwenhuis","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0225","first-page":"335","article-title":"Computing small clause normal forms","volume":"Vol. I","author":"Nonnengart","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0230","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(08)80130-7","article-title":"Using forcing to prove completeness of resolution and paramodulation","volume":"11","author":"Pais","year":"1991","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0235","first-page":"293","article-title":"A structure-preserving clause form translation","volume":"2","author":"Plaisted","year":"1986","journal-title":"JSC"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50004-7_bb0240","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1023\/A:1006376231563","article-title":"Ordered semantic hyper-linking","volume":"25","author":"Plaisted","year":"2000","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0245","article-title":"Building-in equational theories","volume":"7","author":"Plotkin","year":"1972","journal-title":"Machine Intelligence"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0250","unstructured":"Reynolds J. C. [1965], Unpublished seminar notes. Stanford University."},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0255","first-page":"227","article-title":"Automatic deduction with hyper-resolution","volume":"1","author":"Robinson","year":"1965","journal-title":"International J. Computer Mathematics"},{"key":"10.1016\/B978-044450813-3\/50004-7_rf0255","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":"J. Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0265","article-title":"Resolution is a decision procedure for many propositional modal logics","author":"Schmidt","year":"1997","journal-title":"Research Report MPI-I-97-2-002, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50004-7_bb0270","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/321420.321428","article-title":"Automatic theorem proving with renamable and semantic resolution","volume":"14","author":"Slagle","year":"1967","journal-title":"J. the ACM"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0275","series-title":"Proceedings of the 9th International Joint Conference on Artificial Intelligence","first-page":"1181","article-title":"Automated deduction by theory resolution","author":"Stickel","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0280","series-title":"Seminars in Mathematics V.A. Steklov Math. Institute, Leningrad","first-page":"115","article-title":"On the complexity of derivation in propositional calculus","author":"Tseitin","year":"1970"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0285","series-title":"Proc. 12th International Conference on Automated Deduction","first-page":"530","article-title":"Associative-commutative deduction with constraints","author":"Vigneron","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0290","series-title":"Automated Reasoning: 33 Basic Research Problems","author":"Wos","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50004-7_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":"J. Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50004-7_bb0300","article-title":"Reduction, superposition and induction: Automated reasoning in an equational logic","author":"Zhang","year":"1988","journal-title":"PhD thesis, Rensselaer Polytechnic Institute, Schenectady, New York"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50004-7_bb0305","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1006\/jsco.1994.1011","article-title":"A new method for the boolean ring based theorem proving","volume":"17","author":"Zhang","year":"1994","journal-title":"J. Symbolic Computation"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500047?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500047?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T00:54:36Z","timestamp":1556499276000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500047"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":60,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50004-7","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}