{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T01:12:40Z","timestamp":1768093960045,"version":"3.49.0"},"reference-count":18,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3705,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[2003,7]]},"DOI":"10.1016\/s0747-7171(03)00036-1","type":"journal-article","created":{"date-parts":[[2003,5,13]],"date-time":"2003-05-13T01:09:24Z","timestamp":1052788164000},"page":"79-99","source":"Crossref","is-referenced-by-count":6,"title":["Stratified resolution"],"prefix":"10.1016","volume":"36","author":[{"given":"Anatoli","family":"Degtyarev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Nieuwenhuis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0747-7171(03)00036-1_B1","series-title":"Handbook of Theoretical Computer Science","first-page":"493","article-title":"Logic programming","volume":"vol. B","author":"Apt","year":"1990"},{"key":"10.1016\/S0747-7171(03)00036-1_B2","series-title":"Foundations of Deductive Databases and Logic Programming","first-page":"89","article-title":"Towards a theory of declarative knowledge","author":"Apt","year":"1988"},{"key":"10.1016\/S0747-7171(03)00036-1_B3","series-title":"ICLP-91, Logic Programming, Proceedings of the Eighth International Conference","first-page":"645","article-title":"Perfect model semantics for logic programs with equality","author":"Bachmair","year":"1991"},{"key":"10.1016\/S0747-7171(03)00036-1_B4","first-page":"19","article-title":"Resolution theorem proving","volume":"vol. I","author":"Bachmair","year":"2001"},{"issue":"4","key":"10.1016\/S0747-7171(03)00036-1_B5","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1142\/S0129054190000278","article-title":"Solving symbolic ordering constraints","volume":"1","author":"Comon","year":"1990","journal-title":"International Journal of Foundations of Computer Science"},{"key":"10.1016\/S0747-7171(03)00036-1_B6","doi-asserted-by":"crossref","unstructured":"de Nivelle, H., 1996. Ordering Refinements of Resolution. Ph.D. Thesis, Technische Universiteit Delft","DOI":"10.1007\/978-3-7091-9461-4_1"},{"key":"10.1016\/S0747-7171(03)00036-1_B7","series-title":"CADE-17, 17th International Conference on Automated Deduction","first-page":"365","article-title":"Stratified resolution","volume":"vol. 1831","author":"Degtyarev","year":"2000"},{"key":"10.1016\/S0747-7171(03)00036-1_B8","unstructured":"Ganzinger, H., Nieuwenhuis, R., Nivela, P., 2001. The Saturate system. Max-Planck-Institut f\u00fcr Informatik. Maintained and distributed on the Web at: http:\/\/www.mpi-sb.mpg.de\/SATURATE\/Saturate.html"},{"key":"10.1016\/S0747-7171(03)00036-1_B9","series-title":"Automata, Languages and Programming, ICALP\u201991, 18th International Colloquium","first-page":"455","article-title":"Satisfiability of systems of ordinal notations with the subterm property is decidable","volume":"vol. 510","author":"Jouannaud","year":"1991"},{"key":"10.1016\/S0747-7171(03)00036-1_B10","series-title":"Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science","first-page":"291","article-title":"A decision procedure for the existential theory of term algebras with the Knuth\u2013Bendix ordering","author":"Korovin","year":"2000"},{"key":"10.1016\/S0747-7171(03)00036-1_B11","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\/S0747-7171(03)00036-1_B12","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":"Journal of Symbolic Computations"},{"key":"10.1016\/S0747-7171(03)00036-1_B13","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/0020-0190(93)90226-Y","article-title":"Simple LPO constraint solving methods","volume":"47","author":"Nieuwenhuis","year":"1993","journal-title":"Information Processing Letters"},{"key":"10.1016\/S0747-7171(03)00036-1_B14","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rivero, J.M., 1999. Solved forms for path ordering constraints. In: Narendran, P., Rusinowitch, M. (Eds.) RTA, Proceedings of the 10th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science, vol. 1631. Trento, Italy, 2\u20134 July 1999. pp. 1\u201315","DOI":"10.1007\/3-540-48685-2_1"},{"key":"10.1016\/S0747-7171(03)00036-1_B15","first-page":"371","article-title":"Paramodulation-based theorem proving","volume":"vol. I","author":"Nieuwenhuis","year":"2001"},{"key":"10.1016\/S0747-7171(03)00036-1_B16","series-title":"Foundations of Deductive Databases and Logic Programming","first-page":"193","article-title":"On the declarative semantics of deductive databases and logic programs","author":"Przymusinski","year":"1988"},{"key":"10.1016\/S0747-7171(03)00036-1_B17","first-page":"1","article-title":"The design and implementation of Vampire","author":"Riazanov","year":"2002","journal-title":"AI Communications"},{"key":"10.1016\/S0747-7171(03)00036-1_B18","series-title":"Deductive Databases and Logic Programming","first-page":"149","article-title":"Negation as failure using tight derivations for general logic programs","author":"Van Gelder","year":"1988"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717103000361?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717103000361?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T15:56:19Z","timestamp":1553183779000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717103000361"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,7]]},"references-count":18,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2003,7]]}},"alternative-id":["S0747717103000361"],"URL":"https:\/\/doi.org\/10.1016\/s0747-7171(03)00036-1","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[2003,7]]}}}