乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:29:34Z","timestamp":1693610974374},"reference-count":65,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,12,22]],"date-time":"2010-12-22T00:00:00Z","timestamp":1292976000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2011,8]]},"DOI":"10.1007\/s10817-010-9213-y","type":"journal-article","created":{"date-parts":[[2010,12,21]],"date-time":"2010-12-21T06:46:01Z","timestamp":1292913961000},"page":"161-189","source":"Crossref","is-referenced-by-count":30,"title":["On Deciding Satisfiability by Theorem Proving with Speculative Inferences"],"prefix":"10.1007","volume":"47","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[]},{"given":"Christopher A.","family":"Lynch","sequence":"additional","affiliation":[]},{"given":"Leonardo","family":"de Moura","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,12,22]]},"reference":[{"key":"9213_CR1","doi-asserted-by":"crossref","unstructured":"Ernst, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) Proceedings of the Seventh Symposium on Frontiers of Combining Systems (FroCoS). Lecture Notes in Artificial Intelligence, vol. 5749, pp. 84\u201399. Springer (2009)","DOI":"10.1007\/978-3-642-04222-5_5"},{"key":"9213_CR2","doi-asserted-by":"crossref","unstructured":"Vincent, V., Caferra, R., Peltier, N.: A decidable class of nested iterated schemata. In: Giesl, J., H\u00e4hnle, R. (eds.) Proceedings of the Fifth International Joint Conference on Automated Reasoning (IJCAR). Lecture Notes in Artificial Intelligence, vol. 6173, pp. 293\u2013308. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_25"},{"key":"9213_CR3","doi-asserted-by":"crossref","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.) Proceedings of the Fifth Workshop on Frontiers of Combining Systems (FroCoS). Lecture Notes in Artificial Intelligence, vol. 3717, pp. 65\u201380. Springer (2005)","DOI":"10.1007\/11559306_4"},{"issue":"1","key":"9213_CR4","doi-asserted-by":"crossref","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 Trans. Comput. Log. 10(1), 129\u2013179 (2009)","journal-title":"ACM Trans. Comput. Log."},{"issue":"2","key":"9213_CR5","doi-asserted-by":"crossref","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. 183(2), 140\u2013164 (2003)","journal-title":"Inf. Comput."},{"issue":"3","key":"9213_CR6","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"key":"9213_CR7","doi-asserted-by":"crossref","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.) Proceedings of the Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004). Lecture Notes in Computer Science, vol. 3362, pp. 49\u201369. Springer (2005)","DOI":"10.1007\/978-3-540-30569-9_3"},{"issue":"1","key":"9213_CR8","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1145\/363647.363681","volume":"48","author":"DA Basin","year":"2001","unstructured":"Basin, D.A., Ganzinger, H.: Automated complexity analysis based on ordered resolution. J. ACM 48(1), 70\u2013109 (2001)","journal-title":"J. ACM"},{"key":"9213_CR9","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Schmidt, R.A.: Blocking and other enhancements for bottom-up model generation methods. In: Furbach, U., Shankar, N. (eds.) Proceedings of the Third International Joint Conference on Automated Reasoning (IJCAR). Lecture Notes in Artificial Intelligence, vol. 4130, pp. 125\u2013139. Springer (2006)","DOI":"10.1007\/11814771_11"},{"key":"9213_CR10","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P.: A taxonomy of theorem-proving strategies. In: Wooldridge, M.J., Veloso, M. (eds.) Artificial Intelligence Today\u2014Recent Trends and Developments. Lecture Notes in Artificial Intelligence, vol. 1600, pp. 43\u201384. Springer (1999)","DOI":"10.1007\/3-540-48317-9_3"},{"key":"9213_CR11","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P.: On theorem proving for program checking\u2014historical perspective and recent developments. In: Fernandez, M. (ed.) Proceedings of the Twelfth International Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 1\u201311. ACM Press (2010)","DOI":"10.1145\/1836089.1836090"},{"issue":"1","key":"9213_CR12","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1145\/1182613.1182619","volume":"8","author":"MP Bonacina","year":"2007","unstructured":"Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Trans. Comput. Log. 8(1), 180\u2013208 (2007)","journal-title":"ACM Trans. Comput. Log."},{"key":"9213_CR13","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Echenim, M.: $\\mathcal{T}$ -decision by decomposition. In: Pfenning, F. (ed.) Proceedings of the Twenty-First Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 4603, pp. 199\u2013214. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_14"},{"key":"9213_CR14","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Echenim, M.: Rewrite-based decision procedures. In: Archer, M., de la Tour, T.B., Munoz, C. (eds.) Proceedings of the Sixth Workshop on Strategies in Automated Deduction (STRATEGIES), Federated Logic Conference 2006. Electronic Notes in Theoretical Computer Science, vol. 174(11), pp. 27\u201345. Elsevier (2007)","DOI":"10.1016\/j.entcs.2006.11.042"},{"key":"9213_CR15","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Echenim, M.: Rewrite-based satisfiability procedures for recursive data structures. In: Cook, B., Sebastiani, R. (eds.) Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), Federated Logic Conference 2006. Electronic Notes in Theoretical Computer Science, vol. 174(8), pp. 55\u201370. Elsevier (2007)","DOI":"10.1016\/j.entcs.2006.11.039"},{"issue":"1","key":"9213_CR16","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1093\/logcom\/exm055","volume":"18","author":"MP Bonacina","year":"2008","unstructured":"Bonacina, M.P., Echenim, M.: On variable-inactivity and polynomial T-satisfiability procedures. J. Log. Comput. 18(1), 77\u201396 (2008)","journal-title":"J. Log. Comput."},{"issue":"2","key":"9213_CR17","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/j.jsc.2008.10.008","volume":"45","author":"MP Bonacina","year":"2010","unstructured":"Bonacina, M.P., Echenim, M.: Theory decision by decomposition. J. Symb. Comput. 45(2), 229\u2013260 (2010)","journal-title":"J. Symb. Comput."},{"key":"9213_CR18","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson\u2013Oppen and rewrite-based decision procedures. In: Furbach, U., Shankar, N. (eds.) Proceedings of the Third International Joint Conference on Automated Reasoning (IJCAR). Lecture Notes in Artificial Intelligence, vol. 4130, pp. 513\u2013527. Springer (2006)","DOI":"10.1007\/11814771_42"},{"key":"9213_CR19","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0304-3975(94)00187-N","volume":"146","author":"MP Bonacina","year":"1995","unstructured":"Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theoret. Comput. Sci. 146, 199\u2013242 (1995)","journal-title":"Theoret. Comput. Sci."},{"key":"9213_CR20","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by DPLL( $\\Gamma+\\mathcal{T}$ ) and unsound theorem proving. In: Schmidt, R. (ed.) Proceedings of the Twenty-Second Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 5663, pp. 35\u201350. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_3"},{"key":"9213_CR21","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) Proceedings of the Seventh Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 3855, pp. 427\u2013442. Springer (2006)","DOI":"10.1007\/11609773_28"},{"key":"9213_CR22","doi-asserted-by":"crossref","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":"9213_CR23","doi-asserted-by":"crossref","unstructured":"Cantone, D., Zarba, C.G.: A decision procedure for monotone functions over bounded and complete lattices. In: de Swart, H. (ed.) Proc. TARSKI II. Lecture Notes in Artificial Intelligence, vol. 4342, pp. 318\u2013333. Springer (2006)","DOI":"10.1007\/11964810_15"},{"key":"9213_CR24","doi-asserted-by":"crossref","unstructured":"Claessen, K., Lilliestr\u00f6m, A.: Automated inference of finite unsatisfiability. In: Schmidt, R. (ed.) Proceedings of the Twenty-Second Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 5663, pp. 388\u2013403. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_29"},{"issue":"7","key":"9213_CR25","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"9213_CR26","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"9213_CR27","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT-solvers. In: Pfenning, F. (ed.) Proceedings of the Twenty-First Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 4603, pp. 183\u2013198. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"9213_CR28","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Engineering DPLL(T) + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Proceedings of the Fourth International Joint Conference on Automated Reasoning (IJCAR). Lecture Notes in Artificial Intelligence, vol. 5195, pp. 475\u2013490. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_40"},{"key":"9213_CR29","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Model-based theory combination. In: Krsti\u0107, S., Oliveras, A. (eds) Proceedings of the Fifth Workshop on Satisfiability Modulo Theories (SMT), Conference on Automated Verification 2007. Electronic Notes in Theoretical Computer Science, vol. 198(2), pp. 37\u201349. Elsevier (2008)","DOI":"10.1016\/j.entcs.2008.04.079"},{"key":"9213_CR30","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proceedings of the Fourteenth Conference on Tools and algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340 (Springer).","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"3","key":"9213_CR31","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"M Dershowitz","year":"1982","unstructured":"Dershowitz, M.: Orderings for term-rewriting systems. Theore. Comput. Sci. 17(3), 279\u2013301 (1982)","journal-title":"Theore. Comput. Sci."},{"key":"9213_CR32","doi-asserted-by":"crossref","unstructured":"Dershowitz, N.: A maximal-literal unit strategy for Horn clauses. In: Kaplan, S., Okada, M. (eds.) Proceedings of the Second Workshop on Conditional and Typed Term Rewriting Systems (CTRS 1990). Lecture Notes in Computer Science, vol. 516, pp. 14\u201325. Springer (1991)","DOI":"10.1007\/3-540-54317-1_78"},{"issue":"8","key":"9213_CR33","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465\u2013476 (1979)","journal-title":"Commun. ACM"},{"issue":"3","key":"9213_CR34","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"DL Detlefs","year":"2005","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"9213_CR35","doi-asserted-by":"crossref","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) Proceedings of the Eighteenth Conference on Automated Verification (CAV). Lecture Notes in Computer Science, vol. 4144, pp. 81\u201394. Springer (2006)","DOI":"10.1007\/11817963_11"},{"key":"9213_CR36","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: Hendren, L.J. (ed.) ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 234\u2013245 (2002)","DOI":"10.1145\/543552.512558"},{"key":"9213_CR37","doi-asserted-by":"crossref","unstructured":"Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Ghilardi, S., Sebastiani, R. (eds.) Proceedings of the Seventh Symposium on Frontiers of Combining Systems (FroCoS). Lecture Notes in Artificial Intelligence, vol. 5749, pp. 263\u2013278. Springer (2009)","DOI":"10.1007\/978-3-642-04222-5_16"},{"issue":"1","key":"9213_CR38","doi-asserted-by":"crossref","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 40(1), 1\u201316 (1993)","journal-title":"J. ACM"},{"key":"9213_CR39","doi-asserted-by":"crossref","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) Proceedings of the Twenty-First Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 4603, pp. 167\u2013182. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_12"},{"issue":"4","key":"9213_CR40","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1145\/566385.566387","volume":"3","author":"R Givan","year":"2002","unstructured":"Givan, R., McAllester, D.A.: Polynomial-time computation via local inference relations. ACM Trans. Comput. Log. 3(4), 521\u2013541 (2002)","journal-title":"ACM Trans. Comput. Log."},{"key":"9213_CR41","doi-asserted-by":"crossref","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"JY Halpern","year":"1991","unstructured":"Halpern, J.Y.: Presburger arithmetic with unary predicates is $\\pi_1^1$ complete. J. Symb. Log. 56, 637\u2013642 (1991)","journal-title":"J. Symb. Log."},{"issue":"3","key":"9213_CR42","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J Hsiang","year":"1991","unstructured":"Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. J. ACM 38(3), 559\u2013587 (1991)","journal-title":"J. ACM"},{"key":"9213_CR43","doi-asserted-by":"crossref","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proceedings of the Fourteenth Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 4963, pp. 265\u2013281. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_19"},{"key":"9213_CR44","unstructured":"Jacobs, S.: Incremental instance generation in local reasoning. In: Baader, F., Ghilardi, S., Hermann, M., Sattler, U., Sofronie-Stokkermans, V. (eds.) Notes of the First Workshop on Complexity, Expressibility and Decidability (CEDAR). International Joint Conference on Automated Reasoning 2008, pp. 47\u201362 (2008)"},{"key":"9213_CR45","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Proceedings of the Conference on Computational Problems in Abstract Algebras, pp. 263\u2013298. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"9213_CR46","doi-asserted-by":"crossref","unstructured":"Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) Proceedings of the Sixteenth EACSL Annual Conference on Computer Science Logic (CSL). Lecture Notes in Computer Science, vol. 4646, pp. 223\u2013237. Springer (2007)","DOI":"10.1007\/978-3-540-74915-8_19"},{"issue":"1\u20132","key":"9213_CR47","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/S0747-7171(08)80134-4","volume":"11","author":"E Kounalis","year":"1991","unstructured":"Kounalis, E., Rusinowitch, M.: On word problems in Horn theories. J. Symb. Comput. 11(1\u20132), 113\u2013128 (1991)","journal-title":"J. Symb. Comput."},{"key":"9213_CR48","doi-asserted-by":"crossref","unstructured":"Lifschitz, V., Morgenstern, L., Plaisted, D.A.: Knowledge representation and classical logic. In: van Harmelen, F., Lifschitz, V., Porter, B. (eds.) Handbook of Knowledge Representation, vol. 1, pp. 3\u201388. Elsevier (2008)","DOI":"10.1016\/S1574-6526(07)03001-5"},{"key":"9213_CR49","doi-asserted-by":"crossref","unstructured":"Lynch, C.A.: Unsound theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) Proceedings of the Thirteenth EACSL Annual Conference on Computer Science Logic (CSL). Lecture Notes in Computer Science, vol. 3210, pp. 473\u2013487. Springer (2004)","DOI":"10.1007\/978-3-540-30124-0_36"},{"key":"9213_CR50","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1090\/S0002-9947-1937-1501929-X","volume":"42","author":"HM MacNeille","year":"1937","unstructured":"MacNeille, H.M.: Partially ordered sets. Trans. Am. Math. Soc. 42, 416\u2013460 (1937)","journal-title":"Trans. Am. Math. Soc."},{"key":"9213_CR51","unstructured":"McCune, W.W.: Otter 3.3 Reference Manual. Technical Report ANL\/MCS-TM-263, MCS Division, Argonne National Laboratory, Argonne, IL, USA (2003)"},{"key":"9213_CR52","doi-asserted-by":"crossref","unstructured":"McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) Proceedings of the Seventeenth Conference on Automated Verification (CAV). Lecture Notes in Computer Science, vol. 3576, pp. 476\u2013490. Springer (2005)","DOI":"10.1007\/11513988_47"},{"issue":"2","key":"9213_CR53","doi-asserted-by":"crossref","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. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9213_CR54","doi-asserted-by":"crossref","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Data structures with arithmetic constraints: a non-disjoint combination. In: Ghilardi, S., Sebastiani, R. (eds.) Proceedings of the Seventh Symposium on Frontiers of Combining Systems (FroCoS). Lecture Notes in Artificial Intelligence, vol. 5749, pp. 319\u2013334. Springer (2009)","DOI":"10.1007\/978-3-642-04222-5_20"},{"issue":"6","key":"9213_CR55","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-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"9213_CR56","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 371\u2013443. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"9213_CR57","unstructured":"Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. In: Michie, D., Meltzer, R. (eds.) Machine Intelligence, vol. IV, pp. 135\u2013150. Edinburgh University Press (1969)"},{"key":"9213_CR58","first-page":"227","volume":"1","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227\u2013234 (1965)","journal-title":"Int. J. Comput. Math."},{"issue":"1","key":"9213_CR59","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"9213_CR60","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/S0747-7171(08)80131-9","volume":"11","author":"M Rusinowitch","year":"1991","unstructured":"Rusinowitch, M.: Theorem-proving with resolution and superposition. J. Symb. Comput. 11, 21\u201350 (1991)","journal-title":"J. Symb. Comput."},{"key":"9213_CR61","first-page":"141","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. J. Sat. Bool. Model. and Comput. 3, 141\u2013224 (2007)","journal-title":"J. Sat. Bool. Model. and Comput."},{"issue":"4","key":"9213_CR62","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1006\/jsco.1993.1029","volume":"15","author":"W Snyder","year":"1993","unstructured":"Snyder, W.: A fast algorithm for generating reduced ground rewriting systems from a set of ground equations. J. Symb. Comput. 15(4), 415-450 (1993)","journal-title":"J. Symb. Comput."},{"key":"9213_CR63","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) Proceedings of the Twentieth Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 3632, pp. 219\u2013234. Springer (2005)","DOI":"10.1007\/11532231_16"},{"issue":"4\u20136","key":"9213_CR64","first-page":"397","volume":"13","author":"V Sofronie-Stokkermans","year":"2007","unstructured":"Sofronie-Stokkermans, V., Ihlemann, C.: Automated reasoning in some local extensions of ordered structures. J. Mult.-Valued Log. Soft Comput. 13(4\u20136), 397\u2013414 (2007)","journal-title":"J. Mult.-Valued Log. Soft Comput."},{"key":"9213_CR65","doi-asserted-by":"crossref","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) Proceedings of the Seventh Symposium on Frontiers of Combining Systems (FroCoS). Lecture Notes in Artificial Intelligence, vol. 5749, pp. 366\u2013382. Springer (2009)","DOI":"10.1007\/978-3-642-04222-5_23"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9213-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9213-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9213-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T02:51:29Z","timestamp":1559875889000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9213-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12,22]]},"references-count":65,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,8]]}},"alternative-id":["9213"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9213-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,12,22]]}}}