{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:50:08Z","timestamp":1761922208291,"version":"build-2065373602"},"reference-count":25,"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:1005808119103","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:56:21Z","timestamp":1040514981000},"page":"237-246","source":"Crossref","is-referenced-by-count":55,"title":["SETHEO and E-SETHEO - The CADE-13 Systems"],"prefix":"10.1007","volume":"18","author":[{"given":"Max","family":"Moser","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ortrun","family":"Ibens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reinhold","family":"Letz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"Steinbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Goller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johann","family":"Schumann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus","family":"Mayr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"133478_CR1","doi-asserted-by":"crossref","unstructured":"Astrachan, O. L. and Stickel, M. E.: Caching and lemmaizing in model elimination theorem provers, in CADE-11, LNAI 607, Springer, 1992, pp. 224\u2013238.","DOI":"10.1007\/3-540-55602-8_168"},{"issue":"2","key":"133478_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, C. and Snyder, W.: Basic paramodulation, Information and Computation\n121(2) (1995), 172\u2013192.","journal-title":"Information and Computation"},{"key":"133478_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90102-6","volume-title":"Automated Theorem Proving","author":"W. Bibel","year":"1987","unstructured":"Bibel, W.: Automated Theorem Proving, Vieweg Verlag, Braunschweig, 1987."},{"issue":"4","key":"133478_CR4","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"Brand, D.: Proving theorems with the modification method, SIAM Journal of Computing\n4(4) (1975), 412\u2013430.","journal-title":"SIAM Journal of Computing"},{"key":"133478_CR5","doi-asserted-by":"crossref","unstructured":"McCune, W. W. and Wos, L.: Otter: The CADE-13 competition incarnations, Journal of Automated Reasoning\n18(2) (1997).","DOI":"10.1023\/A:1005843632307"},{"key":"133478_CR6","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"67","author":"J. Gallier","year":"1989","unstructured":"Gallier, J. and Snyder, W.: Complete sets of transformations for general E-unification, Theoretical Computer Science\n67 (1989), 203\u2013260.","journal-title":"Theoretical Computer Science"},{"key":"133478_CR7","doi-asserted-by":"crossref","unstructured":"Goller, C., Letz, R., Mayr, K. and Schumann, J.: SETHEO V3.2: Recent developments - system abstract, in CADE-12, LNAI 814, Springer, 1994, pp. 778\u2013782.","DOI":"10.1007\/3-540-58156-1_59"},{"key":"133478_CR8","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Optimizing proof search in model elimination, CADE-13, LNAI 1104, Springer, 1996, pp. 313\u2013327.","DOI":"10.1007\/3-540-61511-3_97"},{"key":"133478_CR9","series-title":"Technical Report","volume-title":"Subgoal Alternation in Model Elimination","author":"O. Ibens","year":"1996","unstructured":"Ibens, O. and Letz, R.: Subgoal Alternation in Model Elimination, Technical Report, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 1996."},{"key":"133478_CR10","doi-asserted-by":"crossref","unstructured":"Knuth, D. E. and Bendix, P. B.: Simple word problems in universal algebras, inConference on Computational Problems in Abstract Algebra, Pergamon Press, 1970, pp. 263\u2013297.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"133478_CR11","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"Letz, R., Mayr, K. and Goller, C.: Controlled integration of the cut rule into connection tableau calculi, Journal of Automated Reasoning\n13 (1994), 297\u2013337.","journal-title":"Journal of Automated Reasoning"},{"key":"133478_CR12","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S. and Bibel, W.: SETHEO: A high-performance theorem prover, Journal of Automated Reasoning\n8 (1992), 183\u2013212.","journal-title":"Journal of Automated Reasoning"},{"key":"133478_CR13","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. W. Loveland","year":"1978","unstructured":"Loveland, D. W.: Automated Theorem Proving: A Logical Basis, North-Holland, New York, 1978."},{"key":"133478_CR14","doi-asserted-by":"crossref","unstructured":"Moser, M.: Improving transformation systems for general E-unification, in RTA-5, LNCS 690, Springer, 1993, pp. 92\u2013105.","DOI":"10.1007\/978-3-662-21551-7_8"},{"key":"133478_CR15","volume-title":"Goal-Directed Reasoning in Clausal Logic with Equality","author":"M. Moser","year":"1996","unstructured":"Moser, M.: Goal-Directed Reasoning in Clausal Logic with Equality, Dissertation, Institut f\u00fcr Informatik, TU M\u00fcnchen, 1996."},{"key":"133478_CR16","series-title":"Technical Report","volume-title":"Compiling Basic Paramodulation to Logic","author":"M. Moser","year":"1996","unstructured":"Moser, M.: Compiling Basic Paramodulation to Logic, Technical Report, Institut f\u00fcr Informatik, TU M\u00fcnchen, 1996. To appear."},{"key":"133478_CR17","series-title":"Technical Report","volume-title":"Model Elimination with Basic Ordered Paramodulation","author":"M. Moser","year":"1995","unstructured":"Moser, M., Lynch, C. and Steinbach, J.:Model Elimination with Basic Ordered Paramodulation, Technical Report AR-95-11, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 1995."},{"issue":"1","key":"133478_CR18","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A.: A machine-oriented logic based on the resolution principle, Journal of the ACM\n12(1) (1965), 23\u201341.","journal-title":"Journal of the ACM"},{"key":"133478_CR19","first-page":"135","volume":"4","author":"G. A. Robinson","year":"1969","unstructured":"Robinson, G. A. and Wos, L.: Paramodulation and theorem proving in first-order theories with equality, Machine Intelligence\n4 (1969), 135\u2013150.","journal-title":"Machine Intelligence"},{"key":"133478_CR20","series-title":"Technical Report","volume-title":"SETHEO V3.3 Reference Manual","author":"J. Schumann","year":"1996","unstructured":"Schumann, J. and Ibens, O.: SETHEO V3.3 Reference Manual, Technical Report, Institut f\u00fcr Informatik, TU M\u00fcnchen, 1996. To appear."},{"key":"133478_CR21","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","volume":"7","author":"R. E. Shostak","year":"1976","unstructured":"Shostak, R. E.: Refutation graphs, Artificial Intelligence\n7 (1976), 51\u201364.","journal-title":"Artificial Intelligence"},{"key":"133478_CR22","doi-asserted-by":"crossref","unstructured":"Smullyan, R. M.: First Order Logic, Springer, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"133478_CR23","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"Stickel, M. E.: A Prolog technology theorem prover: Implementation by an extended Prolog compiler, Journal of Automated Reasoning\n4 (1988), 353\u2013380.","journal-title":"Journal of Automated Reasoning"},{"key":"133478_CR24","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G. and Suttner, C. B.: The results of the CADE-13 ATP system competition, Journal of Automated Reasoning\n18(2) (1997).","DOI":"10.1023\/A:1005824522737"},{"key":"133478_CR25","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Suttner, C. B. and Yemenis, T.: The TPTP problem library, in A. Bundy (ed.), Proc. of the 12th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 814, Springer-Verlag, 1994, pp. 252\u2013266.","DOI":"10.1007\/3-540-58156-1_18"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005808119103.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005808119103\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005808119103.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:45:30Z","timestamp":1749123930000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005808119103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,4]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1997,4]]}},"alternative-id":["133478"],"URL":"https:\/\/doi.org\/10.1023\/a:1005808119103","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1997,4]]}}}