{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:32:42Z","timestamp":1725535962812},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642029585"},{"type":"electronic","value":"9783642029592"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02959-2_3","type":"book-chapter","created":{"date-parts":[[2009,7,25]],"date-time":"2009-07-25T01:02:22Z","timestamp":1248483742000},"page":"35-50","source":"Crossref","is-referenced-by-count":13,"title":["On Deciding Satisfiability by DPLL( $\\Gamma+{\\mathcal T}$ ) and Unsound Theorem Proving"],"prefix":"10.1007","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[]},{"given":"Christopher","family":"Lynch","sequence":"additional","affiliation":[]},{"given":"Leonardo","family":"de Moura","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"3_CR1","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 TOCL\u00a010(1), 129\u2013179 (2009)","journal-title":"ACM TOCL"},{"issue":"2","key":"3_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. Inf. Comput.\u00a0183(2), 140\u2013164 (2003)","journal-title":"Inf. Comput."},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"issue":"1","key":"3_CR4","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1145\/1182613.1182619","volume":"8","author":"M.P. Bonacina","year":"2007","unstructured":"Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM TOCL\u00a08(1), 180\u2013208 (2007)","journal-title":"ACM TOCL"},{"key":"3_CR5","series-title":"ENTCS","first-page":"55","volume-title":"Proc. 4th PDPAR Workshop, FLoC 2006","author":"M.P. Bonacina","year":"2007","unstructured":"Bonacina, M.P., Echenim, M.: Rewrite-based satisfiability procedures for recursive data structures. In: Cook, B., Sebastiani, R. (eds.) Proc. 4th PDPAR Workshop, FLoC 2006. ENTCS, vol.\u00a0174(8), pp. 55\u201370. Elsevier, Amsterdam (2007)"},{"issue":"1","key":"3_CR6","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. Logic and Comput.\u00a018(1), 77\u201396 (2008)","journal-title":"J. Logic and Comput."},{"key":"3_CR7","unstructured":"Bonacina, M.P., Echenim, M.: Theory decision by decomposition. J. Symb. Comput., 1\u201342 (to appear)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/11814771_42","volume-title":"Automated Reasoning","author":"M.P. Bonacina","year":"2006","unstructured":"Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol.\u00a04130, pp. 513\u2013527. Springer, Heidelberg (2006)"},{"key":"3_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-2653-9","volume-title":"Automated Model Building","author":"R. Caferra","year":"2004","unstructured":"Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Kluwer Academic Publishers, Amsterdam (2004)"},{"key":"3_CR10","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/11964810_15","volume-title":"Theory and Applications of Relational Structures as Knowledge Instruments II","author":"D. Cantone","year":"2006","unstructured":"Cantone, D., Zarba, C.G.: A decision procedure for monotone functions over bounded and complete lattices. In: de Swart, H. (ed.) TARSKI 2006. LNCS (LNAI), vol.\u00a04342, pp. 318\u2013333. Springer, Heidelberg (2006)"},{"key":"3_CR11","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-71070-7_40","volume-title":"Automated Reasoning","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Engineering DPLL(T) + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 475\u2013490. Springer, Heidelberg (2008)"},{"key":"3_CR12","series-title":"ENTCS","first-page":"35","volume-title":"Proc. 5th SMT Workshop, CAV 2007","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Model-based theory combination. In: Krsti\u0107, S., Oliveras, A. (eds.) Proc. 5th SMT Workshop, CAV 2007. ENTCS, vol.\u00a0198(2), pp. 35\u201350. Elsevier, Amsterdam (2008)"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proc. PLDI, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"issue":"1","key":"3_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/138027.138032","volume":"40","author":"J. Gallier","year":"1993","unstructured":"Gallier, J., Narendran, P., Plaisted, D.A., Raatz, S., Snyder, W.: Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time. J. ACM\u00a040(1), 1\u201316 (1993)","journal-title":"J. ACM"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"J.Y. Halpern","year":"1991","unstructured":"Halpern, J.Y.: Presburger Arithmetic with unary predicates is $\\Pi_1^1$ Complete. J. Symb. Logic\u00a056, 637\u2013642 (1991)","journal-title":"J. Symb. Logic"},{"key":"3_CR16","unstructured":"Jacobs, S.: Incremental instance generation in local reasoning. In: Notes 1st CEDAR Workshop, IJCAR 2008, pp. 47\u201362 (2008)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-540-30124-0_36","volume-title":"Computer Science Logic","author":"C.A. Lynch","year":"2004","unstructured":"Lynch, C.A.: Unsound theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 473\u2013487. Springer, Heidelberg (2004)"},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1090\/S0002-9947-1937-1501929-X","volume":"42","author":"H.M. MacNeille","year":"1937","unstructured":"MacNeille, H.M.: Partially ordered sets. Transactions of the American Mathematical Society\u00a042, 416\u2013460 (1937)","journal-title":"Transactions of the American Mathematical Society"},{"key":"3_CR19","unstructured":"McCune, W.W.: Otter 3.3 reference manual. Technical Report ANL\/MCS-TM-263, MCS Division, Argonne National Laboratory, Argonne, IL, USA (2003)"},{"issue":"2","key":"3_CR20","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 TOPLAS\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM TOPLAS"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Snyder, W.: A fast algorithm for generating reduced ground rewriting systems from a set of ground equations. J. Symb. Comput. (1992)","DOI":"10.1006\/jsco.1993.1029"},{"key":"3_CR22","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 219\u2013234. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-22"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02959-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T13:51:47Z","timestamp":1558446707000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02959-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642029585","9783642029592"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02959-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}