{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:20:44Z","timestamp":1758979244916},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2007,12,11]],"date-time":"2007-12-11T00:00:00Z","timestamp":1197331200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2008,3]]},"DOI":"10.1007\/s10817-007-9089-7","type":"journal-article","created":{"date-parts":[[2007,12,10]],"date-time":"2007-12-10T16:30:32Z","timestamp":1197304232000},"page":"179-194","source":"Crossref","is-referenced-by-count":6,"title":["Connection Tableaux with Lazy Paramodulation"],"prefix":"10.1007","volume":"40","author":[{"given":"Andrei","family":"Paskevich","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,12,11]]},"reference":[{"issue":"2","key":"9089_CR1","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., Snyder, W.: Basic paramodulation. Inf. Comput. 121(2), 172\u2013192 (1995)","journal-title":"Inf. Comput."},{"key":"9089_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H., Voronkov, A.: Elimination of equality via transformation with ordering constraints. In: Kirchner, C., Kirchner, H. (eds.) Automated Deduction: 15th International Conference, CADE-15. Lecture Notes in Computer Science, vol. 1421, pp. 175\u2013190 (1998)","DOI":"10.1007\/BFb0054259"},{"key":"9089_CR3","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 J. Comput. 4, 412\u2013430 (1975)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"9089_CR4","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1023\/A:1005996623714","volume":"20","author":"A. Degtyarev","year":"1998","unstructured":"Degtyarev, A., Voronkov, A.: What you always wanted to know about rigid E-unification. J. Autom. Reason. 20(1), 47\u201380 (1998)","journal-title":"J. Autom. Reason."},{"key":"9089_CR5","doi-asserted-by":"crossref","unstructured":"Dougherty, D.J., Johann, P.: An improved general E-unification method. In: Stickel, M.E. (ed.) Automated Deduction: 10th International Conference, CADE-10. Lecture Notes in Computer Science, vol. 449, pp. 261\u2013275 (1990)","DOI":"10.1007\/3-540-52885-7_93"},{"key":"9089_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., Snyder, W.: Complete sets of transformations for general E-unification. Theor. Comp. Sci. 67, 203\u2013260 (1989)","journal-title":"Theor. Comp. Sci."},{"key":"9089_CR7","doi-asserted-by":"crossref","unstructured":"Giese, M.: A model generation style completeness proof for constraint tableaux with superposition. In: Egly, U., Ferm\u00fcller, C.G. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX 2002. Lecture Notes in Computer Science, vol. 2381, pp. 130\u2013144 (2002)","DOI":"10.1007\/3-540-45616-3_10"},{"issue":"2","key":"9089_CR8","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., Bibel, W.: SETHEO: a high-performance theorem prover. J. Autom. Reason. 8(2), 183\u2013212 (1992)","journal-title":"J. Autom. Reason."},{"key":"9089_CR9","doi-asserted-by":"crossref","unstructured":"Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook for Automated Reasoning, vol.\u00a0II, Chapt. 28, pp. 2017\u20132116. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50030-8"},{"issue":"3","key":"9089_CR10","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D.W. Loveland","year":"1968","unstructured":"Loveland, D.W.: Mechanical theorem proving by model elimination. J. ACM 16(3), 349\u2013363 (1968)","journal-title":"J. ACM"},{"key":"9089_CR11","unstructured":"Loveland, D.W.: Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science, vol. 6. North-Holland (1978)"},{"key":"9089_CR12","doi-asserted-by":"crossref","unstructured":"Moser, M.: Improving transformation systems for general E-unification. In: Kirchner, C. (ed.) Rewriting Techniques and Applications: 5th International Conference, RTA 1993. Lecture Notes in Computer Science, vol. 690, pp. 92\u2013105 (1993)","DOI":"10.1007\/3-540-56868-9_8"},{"issue":"2","key":"9089_CR13","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M. Moser","year":"1997","unstructured":"Moser, M., Ibens, O., Letz, R., Steinbach, J., Goller, C., Schumann, J., Mayr, K.: SETHEO and E-SETHEO \u2013 the CADE-13 systems. J. Autom. Reason. 18(2), 237\u2013246 (1997)","journal-title":"J. Autom. Reason."},{"key":"9089_CR14","unstructured":"Moser, M., Lynch, C., Steinbach, J.: Model elimination with basic ordered paramodulation. Technical Report AR-95-11, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen (1995)"},{"key":"9089_CR15","unstructured":"Moser, M., Steinbach, J.: STE-modification revisited. Technical Report AR-97-03, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen (1997)"},{"key":"9089_CR16","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook for Automated Reasoning, vol.\u00a0I, Chapt. 7, pp. 371\u2013443. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"9089_CR17","doi-asserted-by":"crossref","unstructured":"Paskevich, A.: Connection tableaux with lazy paramodulation. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning, 3rd International Joint Conference IJCAR 2006. Lecture Notes in Computer Science, vol. 4130, pp. 112\u2013124. Seattle WA, USA (2006)","DOI":"10.1007\/11814771_10"},{"key":"9089_CR18","doi-asserted-by":"crossref","unstructured":"Snyder, W., Lynch, C.: Goal directed strategies for paramodulation. In: Book, R. (ed.) Rewriting Techniques and Applications: 4th International Conference, RTA 1991. Lecture Notes in Computer Science, vol. 488, pp. 150\u2013161 (1991)","DOI":"10.1007\/3-540-53904-2_93"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9089-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-007-9089-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9089-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:48Z","timestamp":1559265708000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-007-9089-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12,11]]},"references-count":18,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2008,3]]}},"alternative-id":["9089"],"URL":"https:\/\/doi.org\/10.1007\/s10817-007-9089-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,12,11]]}}}