{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:42:00Z","timestamp":1747546920791},"publisher-location":"Berlin\/Heidelberg","reference-count":11,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354055727X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0013068","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T02:02:07Z","timestamp":1132711327000},"page":"273-284","source":"Crossref","is-referenced-by-count":12,"title":["Non-clausal resolution and superposition with selection and redundancy criteria"],"prefix":"10.1007","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"}]}],"member":"297","reference":[{"key":"25_CR1","first-page":"427","volume-title":"Lect. Notes in Comp. Sci., vol. 449","author":"L. Bachmair","year":"1990","unstructured":"L. Bachmair and H. Ganzinger, 1990. On Restrictions of Ordered Paramodulation with Simplification. In Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, Lect. Notes in Comp. Sci., vol. 449, pp. 427\u2013441, Berlin-Heidelberg-New York-Tokyo, Springer-Verlag."},{"key":"25_CR2","volume-title":"Research Report 208","author":"L. Bachmair","year":"1991","unstructured":"L. Bachmair and H. Ganzinger, 1991. Rewrite-based equational theorem proving with selection and simplification. Research Report 208, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken. Revised version to appear in the Journal of Logic and Computation."},{"issue":"1","key":"25_CR3","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Nachum Dershowitz, 1987. Termination of Rewriting. J. Symbolic Computation, Vol. 3, No. 1, pp. 69\u2013115.","journal-title":"J. Symbolic Computation"},{"key":"25_CR4","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Z. Manna and R. Waldinger, 1980. A deductive approach to program synthesis. ACM Trans. on Progr. Lang. and Systems, Vol. 2, pp. 90\u2013121.","journal-title":"ACM Trans. on Progr. Lang. and Systems"},{"issue":"1","key":"25_CR5","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0004-3702(82)90011-X","volume":"18","author":"N. V. Murray","year":"1982","unstructured":"Neil V. Murray, 1982. Completely non-clausal theorem proving. Artificial Intelligence, Vol. 18, No. 1, pp. 67\u201385.","journal-title":"Artificial Intelligence"},{"key":"25_CR6","first-page":"293","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"D.A. Plaisted and S. Greenbaum, 1986. A structure-preserving clause form translation. JSC, Vol. 2, pp. 293\u2013304.","journal-title":"JSC"},{"key":"25_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-66473-1","volume-title":"Proof theory","author":"K. Sch\u00fctte","year":"1977","unstructured":"K. Sch\u00fctte, 1977. Proof theory. Springer, Berlin."},{"issue":"4","key":"25_CR8","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"J. R. Slagle","year":"1967","unstructured":"J. R. Slagle, 1967. Automatic Theorem Proving with Renamable and Semantic Resolution. Journal ACM, Vol. 14, No. 4, pp. 687\u2013697.","journal-title":"Journal ACM"},{"issue":"4","key":"25_CR9","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J. R. Slagle","year":"1974","unstructured":"J. R. Slagle, 1974. Automated Theorem-Proving for Theories with Simplifiers, Commutativity, and Associativity. Journal ACM, Vol. 21, No. 4, pp. 622\u2013642.","journal-title":"Journal ACM"},{"key":"25_CR10","first-page":"115","volume-title":"Seminars in Mathematics V.A. Steklov Math. Institute, Leningrad, vol. 8","author":"G. S. Tseitin","year":"1970","unstructured":"G. S. Tseitin, 1970. On the complexity of derivation in propositional calculus. Seminars in Mathematics V.A. Steklov Math. Institute, Leningrad, vol. 8, pp. 115\u2013125. Consultants Bureau, New York \u2014 London."},{"key":"25_CR11","volume-title":"Automated Reasoning: 33 Basic Research Problems","author":"L. Wos","year":"1988","unstructured":"L. Wos, 1988. Automated Reasoning: 33 Basic Research Problems. Prentice-Hall, Englewood Cliffs, New Jersey."}],"container-title":["Lecture Notes in Computer Science","Logic Programming and Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0013068.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T10:06:56Z","timestamp":1607335616000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0013068"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354055727X"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/bfb0013068","relation":{},"subject":[]}}