{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:37:43Z","timestamp":1725550663844},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291077"},{"type":"electronic","value":"9783540320722"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560647_39","type":"book-chapter","created":{"date-parts":[[2005,10,20]],"date-time":"2005-10-20T14:04:06Z","timestamp":1129817046000},"page":"594-608","source":"Crossref","is-referenced-by-count":11,"title":["On Superposition-Based Satisfiability Procedures and Their Combination"],"prefix":"10.1007","author":[{"given":"H\u00e9l\u00e8ne","family":"Kirchner","sequence":"first","affiliation":[]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[]},{"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[]},{"given":"Duc Khanh","family":"Tran","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"39_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/11559306_4","volume-title":"Frontiers of Combining Systems","author":"A. Armando","year":"2005","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 65\u201380. Springer, Heidelberg (2005)"},{"issue":"2","key":"39_CR2","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A Rewriting Approach to Satisfiability Procedures. Info. and Comp.\u00a0183(2), 140\u2013164 (2003)","journal-title":"Info. and Comp."},{"key":"39_CR3","volume-title":"Proc. of the Int. Conf. on Software Engineering and Formal Methods (SEFM 2003)","author":"D. D\u00e9harbe","year":"2003","unstructured":"D\u00e9harbe, D., Ranise, S.: Light-Weight Theorem Proving for Debugging and Verifying Units of Code. In: Proc. of the Int. Conf. on Software Engineering and Formal Methods (SEFM 2003). IEEE Comp. Soc. Press, Los Alamitos (2003)"},{"key":"39_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-540-25984-8_12","volume-title":"Automated Reasoning","author":"E. Denney","year":"2004","unstructured":"Denney, E., Fischer, B., Schumann, J.: Using automated theorem provers to certify auto-generated aerospace software. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 198\u2013212. Springer, Heidelberg (2004)"},{"key":"39_CR5","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Handbook of Theoretical Computer Science, ch.\u00a06. Rewrite Systems, vol.\u00a0B, pp. 244\u2013320. Elsevier Science Publishers B. V. North-Holland (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"39_CR6","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking. Technical Report HPL-2003-148, HP Laboratories (2003)"},{"key":"39_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-45085-6_15","volume-title":"Automated Deduction \u2013 CADE-19","author":"H. Ganzinger","year":"2003","unstructured":"Ganzinger, H., Hillenbrand, T., Waldmann, U.: Superposition modulo a Shostak theory. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 182\u2013196. Springer, Heidelberg (2003)"},{"key":"39_CR8","unstructured":"Kapur, D., Nie, X.: Reasoning about Numbers in Tecton. In: Proc. 8 th Inl. Symp. Methodologies for Intelligent Systems, pp. 57\u201370 (1994)"},{"key":"39_CR9","unstructured":"Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.K.: On Superposition-Based Satisfiability Procedures and their Combination (Full Version), Available at http:\/\/www.loria.fr\/~ranise\/pubs\/long-ictac05.ps.gz"},{"key":"39_CR10","unstructured":"Nelson, G.: Techniques for program verification. Technical Report CS-81-10, Xerox Palo Research Center California USA (1981)"},{"issue":"2","key":"39_CR11","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans.\u00a0on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans.\u00a0on Programming Languages and Systems"},{"key":"39_CR12","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Hand. of Automated Reasoning (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"39_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-31862-0_27","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"S. Ranise","year":"2005","unstructured":"Ranise, S., Ringeissen, C., Tran, D.-K.: Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol.\u00a03407, pp. 372\u2013386. Springer, Heidelberg (2005)"},{"key":"39_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/11559306_3","volume-title":"Frontiers of Combining Systems","author":"S. Ranise","year":"2005","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 48\u201364. Springer, Heidelberg (2005)"},{"issue":"2\/3","key":"39_CR15","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 A Brainiac Theorem Prover. Journal of AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"Journal of AI Communications"},{"key":"39_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. J. of the ACM\u00a031, 1\u201312 (1984)","journal-title":"J. of the ACM"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2005"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560647_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T11:08:23Z","timestamp":1586516903000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560647_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291077","9783540320722"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/11560647_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}