{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:07:46Z","timestamp":1725829666921},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243115"},{"type":"electronic","value":"9783319243122"}],"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-24312-2_7","type":"book-chapter","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T14:06:46Z","timestamp":1441894006000},"page":"86-101","source":"Crossref","is-referenced-by-count":2,"title":["Integrating Simplex with Tableaux"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Bury","sequence":"first","affiliation":[]},{"given":"David","family":"Delahaye","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996) ISBN: 0521496195","DOI":"10.1017\/CBO9780511624162"},{"issue":"3","key":"7_CR2","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H. Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: Autarkic Computations in Formal Proofs. Journal of Automated Reasoning (JAR)\u00a028(3), 321\u2013336 (2002)","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-38574-2_3","volume-title":"Automated Deduction \u2013 CADE-24","author":"P. Baumgartner","year":"2013","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic Superposition with Weak Abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 39\u201357. Springer, Heidelberg (2013)"},{"key":"7_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-75560-9_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Bonichon","year":"2007","unstructured":"Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 151\u2013165. Springer, Heidelberg (2007)"},{"key":"7_CR6","unstructured":"Chv\u00e1tal, V.: Linear Programming. Series of Books in the Mathematical Sciences. W.H. Freeman and Company, New York (1983). ISBN: 0716715872."},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-642-45221-5_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Delahaye","year":"2013","unstructured":"Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol.\u00a08312, pp. 274\u2013290. Springer, Heidelberg (2013)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-662-43652-3_26","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D. Delahaye","year":"2014","unstructured":"Delahaye, D., Dubois, C., March\u00e9, C., Mentr\u00e9, D.: The BWare project: building a proof platform for the automated verification of B proof obligations. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol.\u00a08477, pp. 290\u2013293. Springer, Heidelberg (2014)"},{"issue":"1","key":"7_CR10","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem Proving Modulo. Journal of Automated Reasoning (JAR)\u00a031(1), 33\u201372 (2003)","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"7_CR11","unstructured":"Dutertre, B., De Moura, L.M.: Integrating Simplex with DPLL(T). Technical Report SRI-CSL-06-01, SRI International, May 2006"},{"key":"7_CR12","unstructured":"Gomory, R.: An Algorithm for Integer Solutions to Linear Problems. In: Recent Advances in Mathematical Programming, pp. 269\u2013302 (1963)"},{"key":"7_CR13","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2008) ISBN: 9783540741046 (Germany)"},{"key":"7_CR14","series-title":"Wiley-Interscience Series in Discrete Mathematics and Optimization","volume-title":"Integer and Combinatorial Optimization","author":"G.L. Nemhauser","year":"1999","unstructured":"Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. Wiley-Interscience Series in Discrete Mathematics and Optimization. John Wiley & Sons, Inc, New\u00a0York (1999) ISBN: 9780471359432"},{"key":"7_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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)"},{"issue":"4","key":"7_CR16","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning (JAR)\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"7_CR17","unstructured":"The BWare Project (2012). \n                      \n                        http:\/\/bware.lri.fr\/\n                      \n                      \n                    ."},{"key":"7_CR18","unstructured":"The Coq Development Team. Coq, version 8.4pl6. Inria (April 2015), \n                      \n                        http:\/\/coq.inria.fr\/"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24312-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:49:09Z","timestamp":1559256549000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24312-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243115","9783319243122"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24312-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}