{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,10]],"date-time":"2026-11-10T22:13:50Z","timestamp":1794348830283,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540746201","type":"print"},{"value":"9783540746218","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74621-8_16","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T07:46:32Z","timestamp":1187768792000},"page":"237-251","source":"Crossref","is-referenced-by-count":1,"title":["Combining Proof-Producing Decision Procedures"],"prefix":"10.1007","author":[{"given":"Silvio","family":"Ranise","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Duc-Khanh","family":"Tran","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"6","key":"16_CR1","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1006\/jsco.1993.1066","volume":"16","author":"A. Boudet","year":"1993","unstructured":"Boudet, A.: Combining unification algorithms. Journal of Symbolic Computation\u00a016(6), 597\u2013626 (1993)","journal-title":"Journal of Symbolic Computation"},{"issue":"204","key":"16_CR2","first-page":"1411","volume":"10","author":"M. Bozzano","year":"2006","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Ranise, S., Sebastiani, R.: Efficient Theory Combination via Boolean Search. J. of Information and Computation\u00a010(204), 1411\u20131596 (2006)","journal-title":"J. of Information and Computation"},{"issue":"3-4","key":"16_CR3","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF02127968","volume":"17","author":"J. Burg","year":"1996","unstructured":"Burg, J., Lang, S.-D., Hughes, C.E.: Intelligent Backtracking in CLP(R). Ann. Math. Artif. Intell.\u00a017(3-4), 189\u2013211 (1996)","journal-title":"Ann. Math. Artif. Intell."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"de Moura, L., Rue\u00df, H., Shankar, N.: Justifying Equality. In: Proc. of the Workshop on Pragmatics of Decision Procedures for Automated Reasoning (PDPAR 2004), Also in ENTCS, vol. 125(3) (2004)","DOI":"10.1007\/978-3-540-25984-8_14"},{"issue":"4","key":"16_CR5","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P.J. Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM\u00a027(4), 758\u2013771 (1980)","journal-title":"J. ACM"},{"key":"16_CR6","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"1972","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, San Diego (1972)"},{"key":"16_CR7","unstructured":"Fontaine, P.: Techniques for Verification of Concurrent Systems with Invariants. PhD thesis, Universit\u00e9 de Li\u00e8ge (2004)"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.-Y., Merz, S., Prensa Nieto, L., Tiu, A.F.: Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 167\u2013181. Springer, Heidelberg (2006)"},{"key":"16_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"542","DOI":"10.1007\/11916277_37","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H. Kirchner","year":"2006","unstructured":"Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: Automatic Combinability of Rewriting-Based Satisfiability Procedures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 542\u2013556. Springer, Heidelberg (2006)"},{"issue":"2","key":"16_CR10","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. on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1007\/978-3-540-32033-3_33","volume-title":"Term Rewriting and Applications","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-Producing Congruence Closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 453\u2013468. Springer, Heidelberg (2005)"},{"key":"16_CR12","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1016\/S0747-7171(08)80145-9","volume":"12","author":"T. Nipkow","year":"1991","unstructured":"Nipkow, T.: Combining matching algorithms: The regular case. Journal of Symbolic Computation\u00a012, 633\u2013653 (1991)","journal-title":"Journal of Symbolic Computation"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2005)"},{"issue":"6","key":"16_CR14","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1109\/MIS.2006.117","volume":"21","author":"S. Ranise","year":"2006","unstructured":"Ranise, S., Tinelli, C.: Satisfiability Modulo Theories. IEEE Magazine on Intelligent Systems\u00a021(6), 71\u201381 (2006)","journal-title":"IEEE Magazine on Intelligent Systems"},{"key":"16_CR15","volume-title":"Theory of linear and integer programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons, Chichester (1986)"},{"key":"16_CR16","unstructured":"Schulz, S.: E \u2013 a brainiac theorem prover. AI Communications (2002)"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/978-3-540-32033-3_34","volume-title":"Term Rewriting and Applications","author":"A. Stump","year":"2005","unstructured":"Stump, A., Tang, L.-Y.: The Algebra of Equality Proofs. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 469\u2013483. Springer, Heidelberg (2005)"},{"issue":"2","key":"16_CR18","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"R.E. Tarjan","year":"1975","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. of the ACM\u00a022(2), 215\u2013225 (1975)","journal-title":"J. of the ACM"},{"key":"16_CR19","unstructured":"Tran, D.-K.: Conception de Proc\u00e9dures de D\u00e9cision par Combinaison et Saturation. PhD thesis, Universit\u00e9 Henri Poincar\u00e9, Nancy, France, Ch.\u00a08 (in english) (2007)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74621-8_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T17:35:10Z","timestamp":1683999310000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74621-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540746201","9783540746218"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74621-8_16","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-74621-8","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}