{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:10:30Z","timestamp":1748664630935,"version":"3.41.0"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319242453"},{"type":"electronic","value":"9783319242460"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_14","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T04:20:53Z","timestamp":1442636453000},"page":"220-236","source":"Crossref","is-referenced-by-count":0,"title":["Axiomatic Constraint Systems for Proof Search Modulo Theories"],"prefix":"10.1007","author":[{"given":"Damien","family":"Rouhling","sequence":"first","affiliation":[]},{"given":"Mahfuza","family":"Farooque","sequence":"additional","affiliation":[]},{"given":"St\u00e9phane","family":"Graham-Lengrand","sequence":"additional","affiliation":[]},{"given":"Assia","family":"Mahboubi","sequence":"additional","affiliation":[]},{"given":"Jean-Marc","family":"Notin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/978-3-540-89439-1_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Baumgartner","year":"2008","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: ME(LIA) \u2013 Model evolution with linear integer arithmetic constraints. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 258\u2013273. Springer, Heidelberg (2008)"},{"key":"14_CR2","unstructured":"Baumgartner, P., Furbach, U., Petermann, U.: A unified approach to theory reasoning. Technical report, Inst. f\u00fcr Informatik, Univ. (1992)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-642-22438-6_9","volume-title":"Automated Deduction \u2013 CADE-23","author":"P. Baumgartner","year":"2011","unstructured":"Baumgartner, P., Tinelli, C.: Model evolution with equality modulo built-in theories. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 85\u2013100. Springer, Heidelberg (2011)"},{"key":"14_CR4","unstructured":"Beckert, B.: Chapter 8: Rigid E-unification. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction \u2013 A Basis for Applications. Foundations. Calculi and Methods, vol.\u00a0I, pp. 265\u2013289. Kluwer Academic Publishers (1998)"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Beckert, B.: Equality and other theories. In: Handbook of Tableau Methods, pp. 197\u2013254. Kluwer Academic Publishers (1999)","DOI":"10.1007\/978-94-017-1754-0_4"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Dross, C., Conchon, S., Kanig, J., Paskevich, A.: Reasoning with triggers. In: Fontaine, P., Goel, A. (eds.) 10th Int. Work. on Satisfiability Modulo Theories, SMT 2012. EPiC Series, vol.\u00a020, pp. 22\u201331. EasyChair, June 2012","DOI":"10.29007\/3c1n"},{"key":"14_CR7","unstructured":"Ganzinger, H., RueB, H., Shankar, N.: Modularity and refinement in inference systems. Technical Report SRI-CSL-04-02, SRI (2004)"},{"key":"14_CR8","first-page":"227","volume-title":"3rd Int. Work. on First-Order Theorem Proving (FTP)","author":"M. Giese","year":"2000","unstructured":"Giese, M.: Proof search without backtracking using instance streams, position paper. In: Baumgartner, P., Zhang, H. (eds.) 3rd Int. Work. on First-Order Theorem Proving (FTP), pp. 227\u2013228. Univ. of Koblenz, St. Andrews (2000)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","first-page":"37","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M. Giese","year":"2003","unstructured":"Giese, M., H\u00e4hnle, R.: Tableaux + constraints. In: Cialdea Mayer, M., Pirri, F. (eds.) TABLEAUX 2003. LNCS, vol.\u00a02796, pp. 37\u201342. Springer, Heidelberg (2003)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/978-3-642-40537-2_14","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S. Graham-Lengrand","year":"2013","unstructured":"Graham-Lengrand, S.: Psyche: A proof-search engine based on sequent calculus with an LCF-Style architecture. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol.\u00a08123, pp. 149\u2013156. Springer, Heidelberg (2013)"},{"issue":"6","key":"14_CR11","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J. of the ACM Press\u00a053(6), 937\u2013977 (2006)","journal-title":"J. of the ACM Press"},{"key":"14_CR12","unstructured":"Psyche: the Proof-Search factorY for Collaborative HEuristics"},{"key":"14_CR13","unstructured":"Rouhling, D., Farooque, M., Graham-Lengrand, S., Notin, J.-M., Mahboubi, A.: Axiomatisation of constraint systems to specify a tableaux calculus modulo theories. Technical report, Laboratoire d\u2019informatique de l\u2019\u00c9cole Polytechnique - CNRS, Microsoft Research - INRIA Joint Centre, Parsifal & TypiCal - INRIA Saclay, France, December 2014"},{"key":"14_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 274\u2013289. Springer, Heidelberg (2008)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Saraswat, V.A., Rinard, M., Panangaden, P.: The semantic foundations of concurrent constraint programming. In: Wise, D.S. (ed.) 18th Annual ACM Symp. on Principles of Programming Languages (POPL 1991), pp. 333\u2013352. ACM Press, January 1991","DOI":"10.1145\/99583.99627"},{"issue":"4","key":"14_CR16","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M.E. Stickel","year":"1985","unstructured":"Stickel, M.E.: Automated deduction by theory resolution. J. of Automated Reasoning\u00a01(4), 333\u2013355 (1985)","journal-title":"J. of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T18:26:27Z","timestamp":1748629587000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}