{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:32:54Z","timestamp":1725471174040},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_10","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"112-124","source":"Crossref","is-referenced-by-count":2,"title":["Connection Tableaux with Lazy Paramodulation"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Paskevich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"10_CR1","doi-asserted-by":"publisher","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. Journal of the ACM\u00a016(3), 349\u2013363 (1968)","journal-title":"Journal of the ACM"},{"issue":"2","key":"10_CR2","doi-asserted-by":"publisher","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. Journal of Automated Reasoning\u00a08(2), 183\u2013212 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR3","first-page":"2017","volume-title":"Handbook for Automated Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook for Automated Reasoning, vol.\u00a0II, pp. 2017\u20132116. Elsevier Science, Amsterdam (2001)"},{"key":"10_CR4","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook for Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook for Automated Reasoning, vol.\u00a0I, pp. 371\u2013443. Elsevier Science, Amsterdam (2001)"},{"issue":"1","key":"10_CR5","doi-asserted-by":"publisher","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. Journal of Automated Reasoning\u00a020(1), 47\u201380 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/3-540-45616-3_10","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M. Giese","year":"2002","unstructured":"Giese, M.: A model generation style completeness proof for constraint tableaux with superposition. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 130\u2013144. Springer, Heidelberg (2002)"},{"key":"10_CR7","series-title":"Fundamental studies in Computer Science","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D.W. Loveland","year":"1978","unstructured":"Loveland, D.W.: Automated Theorem Proving: A Logical Basis. Fundamental studies in Computer Science, vol.\u00a06. North-Holland, Amsterdam (1978)"},{"issue":"2","key":"10_CR8","doi-asserted-by":"publisher","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 \u2014 the CADE-13 systems. Journal of Automated Reasoning\u00a018(2), 237\u2013246 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR9","doi-asserted-by":"publisher","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\u00a04, 412\u2013430 (1975)","journal-title":"SIAM Journal of Computing"},{"key":"10_CR10","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":"10_CR11","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-15","author":"L. Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H., Voronkov, A.: Elimination of equality via transformation with ordering constraints. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, Springer, Heidelberg (1998)"},{"key":"10_CR12","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":"10_CR13","doi-asserted-by":"publisher","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. Theoretical Computer Science\u00a067, 203\u2013260 (1989)","journal-title":"Theoretical Computer Science"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1007\/3-540-53904-2_93","volume-title":"Rewriting Techniques and Applications","author":"W. Snyder","year":"1991","unstructured":"Snyder, W., Lynch, C.: Goal directed strategies for paramodulation. In: Book, R.V. (ed.) RTA 1991. LNCS, vol.\u00a0488, pp. 150\u2013161. Springer, Heidelberg (1991)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/3-540-56868-9_8","volume-title":"Rewriting Techniques and Applications","author":"M. Moser","year":"1993","unstructured":"Moser, M.: Improving transformation systems for general E-unification. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol.\u00a0690, pp. 92\u2013105. Springer, Heidelberg (1993)"},{"issue":"2","key":"10_CR16","doi-asserted-by":"publisher","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. Information and computation\u00a0121(2), 172\u2013192 (1995)","journal-title":"Information and computation"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/3-540-52885-7_93","volume-title":"10th International Conference on Automated Deduction","author":"D.J. Dougherty","year":"1990","unstructured":"Dougherty, D.J., Johann, P.: An improved general E-unification method. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 261\u2013275. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:27:33Z","timestamp":1619508453000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11814771_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}