{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:49:01Z","timestamp":1725558541141},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642141270"},{"type":"electronic","value":"9783642141287"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14128-7_6","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T06:45:36Z","timestamp":1277793936000},"page":"49-63","source":"Crossref","is-referenced-by-count":1,"title":["Instantiation of SMT Problems Modulo Integers"],"prefix":"10.1007","author":[{"given":"Mnacho","family":"Echenim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"6_CR1","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.jsc.2009.03.003","volume":"45","author":"A. Abadi","year":"2010","unstructured":"Abadi, A., Rabinovich, A., Sagiv, M.: Decidable fragments of many-sorted logic. Journal of Symbolic Computation\u00a045(2), 153\u2013172 (2010)","journal-title":"Journal of Symbolic Computation"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/978-3-642-04222-5_5","volume-title":"FroCoS 2009","author":"E. Althaus","year":"2009","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic sup(la). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 84\u201399. Springer, Heidelberg (2009)"},{"issue":"1","key":"6_CR3","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/1459010.1459014","volume":"10","author":"A. Armando","year":"2009","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Transactions on Computational Logic\u00a010(1), 129\u2013179 (2009)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"2","key":"6_CR4","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. Information and Computation\u00a0183(2), 140\u2013164 (2003)","journal-title":"Information and Computation"},{"issue":"4","key":"6_CR5","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"3","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation\u00a03(4), 217\u2013247 (1994)","journal-title":"Journal of Logic and Computation"},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierachic first-order theories. Appl. Algebra. Eng. Commun. Comput.\u00a05, 193\u2013212 (1994)","journal-title":"Appl. Algebra. Eng. Commun. Comput."},{"key":"6_CR7","first-page":"825","volume-title":"Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, ch. 26","author":"C. Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, ch. 26, vol.\u00a0185, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"issue":"1","key":"6_CR8","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1093\/logcom\/exm055","volume":"18","author":"M.P. Bonacina","year":"2008","unstructured":"Bonacina, M.P., Echenim, M.: On variable-inactivity and polynomial T-satisfiability procedures. J. of Logic and Computation\u00a018(1), 77\u201396 (2008)","journal-title":"J. of Logic and Computation"},{"issue":"2","key":"6_CR9","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.jsc.2008.10.008","volume":"45","author":"M.P. Bonacina","year":"2010","unstructured":"Bonacina, M.P., Echenim, M.: Theory decision by decomposition. Journal of Symbolic Computation\u00a045(2), 229\u2013260 (2010)","journal-title":"Journal of Symbolic Computation"},{"key":"6_CR10","volume-title":"The Calculus of Computation: Decision Procedures with Applications to Verification","author":"A.R. Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, New York (2007)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Echenim, M., Peltier, N.: A new instantiation scheme for Satisfiability Modulo Theories. Technical report, LIG, CAPP group (2009), \n                    \n                      http:\/\/membres-lig.imag.fr\/peltier\/rr-smt.pdf","DOI":"10.1007\/s10817-010-9200-3"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-540-30124-0_9","volume-title":"Computer Science Logic","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Korovin, K.: Integrating equational reasoning into instantiation-based theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 71\u201384. Springer, Heidelberg (2004)"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y. Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.M.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol.\u00a05643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"issue":"3-4","key":"6_CR14","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/s10472-007-9078-x","volume":"50","author":"S. Ghilardi","year":"2007","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell.\u00a050(3-4), 231\u2013254 (2007)","journal-title":"Ann. Math. Artif. Intell."},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K. Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 223\u2013237. Springer, Heidelberg (2007)"},{"key":"6_CR16","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF00247825","volume":"9","author":"S. Lee","year":"1992","unstructured":"Lee, S., Plaisted, D.A.: Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning\u00a09, 25\u201342 (1992)","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"6_CR17","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"D.A. Plaisted","year":"2000","unstructured":"Plaisted, D.A., Zhu, Y.: Ordered semantic hyperlinking. Journal of Automated Reasoning\u00a025(3), 167\u2013217 (2000)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14128-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:23:13Z","timestamp":1558279393000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14128-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141270","9783642141287"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14128-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}