{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:53:09Z","timestamp":1725551589326},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540305538"},{"type":"electronic","value":"9783540316503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11591191_21","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T09:44:25Z","timestamp":1132652665000},"page":"292-306","source":"Crossref","is-referenced-by-count":0,"title":["Regular Derivations in Basic Superposition-Based Calculi"],"prefix":"10.1007","author":[{"given":"Vladimir","family":"Aleksi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anatoli","family":"Degtyarev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Aleksi\u0107, V., Degtyarev, A.: On arbitrary selection strategies for superposition. Proceedings of FTP, Technical Report of the University of Koblenz (September 2005)","DOI":"10.1007\/11853886_4"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1007\/3-540-55602-8_185","volume-title":"Automated Deduction - CADE-11","author":"L. Bachmair","year":"1992","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation and superposition. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 462\u2013476. Springer, Heidelberg (1992)"},{"key":"21_CR3","unstructured":"Bachmair, L., Ganzinger, H.: Strict basic superposition and chaining. Research report MPI-I-97-2-011, Max-Planck-Institut f\u00fcr Informatic, Saarbr\u00fccken"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"951","DOI":"10.1007\/3-540-48224-5_77","volume-title":"Automata, Languages and Programming","author":"L. Bofill","year":"2001","unstructured":"Bofill, L., Godoy, G.: On the completeness of arbitrary selection strategies for paramoduletion. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 951\u2013962. Springer, Heidelberg (2001)"},{"key":"21_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/3-540-45620-1_36","volume-title":"Automated Deduction - CADE-18","author":"L. Bofill","year":"2002","unstructured":"Bofill, L., Rubio, A.: Well-foundedness is sufficient for completeness of ordered paramodulation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 456\u2013470. Springer, Heidelberg (2002)"},{"key":"21_CR6","first-page":"613","volume-title":"Handbook of Automated Reasoning","author":"A. Degtyarev","year":"2001","unstructured":"Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 613\u2013706. Elsevier Science Publishers B.V, Amsterdam (2001)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/3-540-60983-0_8","volume-title":"Extensions of Logic Programming","author":"A. Degtyarev","year":"1996","unstructured":"Degtyarev, A., Voronkov, A.: Handling equality in logic programs via basic folding. In: Herre, H., Dyckhoff, R., Schroeder-Heister, P. (eds.) ELP 1996. LNCS, vol.\u00a01050, pp. 119\u2013136. Springer, Heidelberg (1996)"},{"key":"21_CR8","first-page":"364","volume-title":"Automation of Reasoning. Classical Papers on Computational Logic","author":"S. Kanger","year":"1963","unstructured":"Kanger, S.: A simplified proof method for elementary logic. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning. Classical Papers on Computational Logic, vol.\u00a01, pp. 364\u2013371. Springer, Heidelberg (1963) (Originally appeared in 1963)"},{"key":"21_CR9","unstructured":"Moser, M., Lynch, C., Steinbach, J.: Model Elimination with Basic Ordered Paramodulation."},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Lynch, C.: Oriented Equational Logic is Complete. Journal of Symbolic Computations, 23(1):23\u201345 (1997). Technical Report AR-95-11, TU M\u00fcnchen (1995)","DOI":"10.1006\/jsco.1996.0075"},{"key":"21_CR11","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 \u201992","author":"R. Nieuwenhuis","year":"1992","unstructured":"Nieuwenhuis, R., Rubio, A.: Basic superposition is complete. In: Krieg-Br\u00fcckner, B. (ed.) ESOP 1992. LNCS, vol.\u00a0582, pp. 371\u2013389. Springer, Heidelberg (1992)"},{"key":"21_CR12","first-page":"3","volume-title":"Handbook of Automated Reasoning","author":"R. Nieuwenhuis","year":"1999","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 3\u201373. Elsevier Science Publishers B.V, Amsterdam (1999)"},{"key":"21_CR13","unstructured":"de Nivelle, H.: Ordering refinements of resolution. Dissertation, Technische Universiteit Delft, Delft (1996)"},{"issue":"1","key":"21_CR14","first-page":"159","volume":"34","author":"G. Robinson","year":"1969","unstructured":"Robinson, G., Wos, L.: Completeness of paramodulation. Journal of Symbolic Logic\u00a034(1), 159\u2013160 (1969)","journal-title":"Journal of Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11591191_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:02:27Z","timestamp":1605643347000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11591191_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540305538","9783540316503"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/11591191_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}