{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:56Z","timestamp":1749182816175,"version":"3.41.0"},"reference-count":7,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1997,4,1]],"date-time":"1997-04-01T00:00:00Z","timestamp":859852800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,4,1]],"date-time":"1997-04-01T00:00:00Z","timestamp":859852800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1997,4]]},"DOI":"10.1023\/a:1005812220011","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:56:21Z","timestamp":1040514981000},"page":"247-252","source":"Crossref","is-referenced-by-count":33,"title":["SPASS - Version 0.49"],"prefix":"10.1007","volume":"18","author":[{"given":"Christoph","family":"Weidenbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"133480_CR1","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L. and Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification, Journal of Logic and Computation\n4(3) (1994), 217\u2013247. Revised version of Max-Planck-Institut f\u00fcr Informatik Technical Report, MPI-I-91-208, 1991.","journal-title":"Journal of Logic and Computation"},{"issue":"2","key":"133480_CR2","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Lynch, Ch. and Snyder, W.: Basic paramodulation, Information and Computation\n121(2) (1995), 172\u2013192. Revised version of Max-Planck-Institut f\u00fcur Informatik Technical Report, MPI-I-93-236, 1993.","journal-title":"Information and Computation"},{"key":"133480_CR3","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R. and Rubio, A.: Theorem proving with ordering and equality constrained clauses, Journal of Symbolic Computation\n19 (1995), 321\u2013351.","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"133480_CR4","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. E. Peterson","year":"1983","unstructured":"Peterson, G. E.: A technique for establishing completeness results in theorem proving with equality, SIAM Journal of Computation\n12(1) (1983), 82\u2013100.","journal-title":"SIAM Journal of Computation"},{"key":"133480_CR5","unstructured":"Weidenbach, Ch.: Extending the resolution method with sorts, in Proc. of 13th International Joint Conference on Artificial Intelligence, IJCAI-93, Morgan Kaufmann, 1993, pp. 60\u201365."},{"key":"133480_CR6","doi-asserted-by":"crossref","unstructured":"Weidenbach, Ch.: Unification in pseudo-linear sort theories is decidable, in M. A. McRobbie and J. K. Slaney (eds), 13th International Conference on Automated Deduction, CADE-13, LNAI 1104, Springer, 1996, pp. 343\u2013357.","DOI":"10.1007\/3-540-61511-3_99"},{"key":"133480_CR7","doi-asserted-by":"crossref","unstructured":"Weidenbach, Ch., Gaede, B. and Rock, G.: SPASS and FLOTTER, version 0.42, in M. A. McRobbie and J. K. Slaney (eds), 13th International Conference on Automated Deduction, CADE-13, LNAI 1104, Springer, 1996, pp. 141\u2013145.","DOI":"10.1007\/3-540-61511-3_75"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005812220011.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005812220011\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005812220011.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:44:56Z","timestamp":1749123896000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005812220011"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,4]]},"references-count":7,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1997,4]]}},"alternative-id":["133480"],"URL":"https:\/\/doi.org\/10.1023\/a:1005812220011","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1997,4]]}}}