{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:41Z","timestamp":1749124061780,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054258","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"160-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Strict basic superposition"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[]},{"given":"Harald","family":"Ganzinger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"19_CR1","first-page":"427","volume-title":"Vol. 449 of Lecture Notes in Computer Science","author":"L. Bachmair","year":"1990","unstructured":"Bachmair, L. & Ganzinger, H. (1990), On restrictions of ordered paramodulation with simplification, in M. Stickel, ed., \u2018Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern', Vol. 449 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 427\u2013441."},{"issue":"3","key":"19_CR2","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L. & Ganzinger, H. (1994), \u2018Rewrite-based equational theorem proving with selection and simplification', J. Logic and Computation 4(3), 217\u2013247. Revised version of Technical Report MPI-I-91-208, 1991.","journal-title":"J. Logic and Computation"},{"key":"19_CR3","volume-title":"Research Report MPI-I-95-2-009","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L. & Ganzinger, H. (1995), Ordered chaining calculi for first-order theories of binary relations, Research Report MPI-I-95-2-009, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Saarbr\u00fccken. Revised version to appear in JACM. URL: www.mpi-sb.mpg.de\/~hg\/pra.html#MPI-I-95-2-009"},{"key":"19_CR4","volume-title":"Research Report MPI-I-97-2-011","author":"L. Bachmair","year":"1997","unstructured":"Bachmair, L. & Ganzinger, H. (1997), Strict basic superposition and chaining, Research Report MPI-I-97-2-011, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Saarbr\u00fccken. URL: www.mpi-sb.mpg.de\/~hg\/pra.html#MPI-I-97-2-011"},{"key":"19_CR5","first-page":"462","volume-title":"Vol. 607 of Lecture Notes in Computer Science","author":"L. Bachmair","year":"1992","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C. & Snyder, W. (1992), Basic paramodulation and superposition, in D. Kapur, ed., \u2018Automated Deduction \u2014 CADE'11', Vol. 607 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 462\u2013476."},{"key":"19_CR6","volume-title":"Research Report MPI-I-97-2-012","author":"L. Bachmair","year":"1997","unstructured":"Bachmair, L., Ganzinger, H. & Voronkov, A. (1997), Elimination of equality via transformation with ordering constraints, Research Report MPI-I-97-2-012, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Saarbr\u00fccken. URL: www.mpi-sb.mpg.de\/~hg\/pra.html#MPI-I-97-2-012"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"Brand, D. (1975), \u2018Proving theorems with the modification method', SIAM J. Comput.\n                        4, 412\u2013430.","journal-title":"SIAM J. Comput."},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/3-540-55253-7_22","volume-title":"ESOP'92","author":"R. Nieuwenhuis","year":"1992","unstructured":"Nieuwenhuis, R. & Rubio, A. (1992a), Basic superposition is complete, in \u2018ESOP'92', Vol. 582 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 371\u2013389."},{"key":"19_CR9","first-page":"477","volume-title":"Vol. 607 of Lecture Notes in Computer Science","author":"R. Nieuwenhuis","year":"1992","unstructured":"Nieuwenhuis, R. & Rubio, A. (1992b), Theorem proving with ordering constrained clauses, in \u2018Automated Deduction \u2014 CADE'11', Vol. 607 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 477\u2013491."},{"key":"19_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0747-7171(08)80130-7","volume":"11","author":"J. Pais","year":"1991","unstructured":"Pais, J. & Peterson, G. (1991), \u2018Using forcing to prove completeness of resolution and paramodulation', J. Symbolic Computation\n                        11, 3\u201319.","journal-title":"J. Symbolic Computation"},{"key":"19_CR11","volume-title":"PhD thesis","author":"H. Zhang","year":"1988","unstructured":"Zhang, H. (1988), Reduction, superposition and induction: Automated reasoning in an equational logic, PhD thesis, Rensselaer Polytechnic Institute, Schenectady, New York."},{"key":"19_CR12","first-page":"1","volume-title":"Vol. 310 of Lecture Notes in Computer Science","author":"H. Zhang","year":"1988","unstructured":"Zhang, H. & Kapur, D. (1988), First-order theorem proving using conditional rewrite rules, in E. Lusk & R. Overbeek, eds, \u2018Proc. 9th Int. Conf. on Automated Deduction', Vol. 310 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 1\u201320."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054258","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T18:39:04Z","timestamp":1676054344000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0054258"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/bfb0054258","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"25 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}