{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:36:37Z","timestamp":1725903397518},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_25","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T09:34:07Z","timestamp":1499679247000},"page":"398-412","source":"Crossref","is-referenced-by-count":4,"title":["Scalable Fine-Grained Proofs for Formula\u00a0Processing"],"prefix":"10.1007","author":[{"given":"Haniel","family":"Barbosa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jasmin Christian","family":"Blanchette","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to COQ through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135\u2013150. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-25379-9_12"},{"key":"25_CR2","unstructured":"Barbosa, H., Blanchette, J.C., Fontaine, P.: Technical report associated with this paper (2017). \nhttps:\/\/hal.inria.fr\/hal-01526841"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-662-54580-5_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2017","unstructured":"Barbosa, H., Fontaine, P., Reynolds, A.: Congruence closure with free variables. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 214\u2013230. Springer, Heidelberg (2017). doi:\n10.1007\/978-3-662-54580-5_13"},{"key":"25_CR4","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: Version 2.5. Technical report, University of Iowa (2015). \nhttp:\/\/smt-lib.org\/"},{"key":"25_CR5","unstructured":"Besson, F., Fontaine, P., Th\u00e9ry, L.: A flexible proof format for SMT: a proposal. In: Fontaine, P., Stump, A. (eds.) PxTP 2011, pp. 15\u201326 (2011)"},{"issue":"2","key":"25_CR6","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-015-9335-3","volume":"56","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., B\u00f6hme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Autom. Reasoning 56(2), 155\u2013200 (2016). doi:\n10.1007\/s10817-015-9335-3","journal-title":"J. Autom. Reasoning"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179\u2013194. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-14052-5_14"},{"key":"25_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., de Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-02959-2_12"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-642-22438-6_18","volume-title":"CADE-23","author":"D D\u00e9harbe","year":"2011","unstructured":"D\u00e9harbe, D., Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Exploiting symmetry in SMT problems. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 222\u2013236. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-22438-6_18"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-319-40229-1_20","volume-title":"Automated Reasoning","author":"G Ebner","year":"2016","unstructured":"Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System description: GAPT 2.0. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 293\u2013301. Springer, Cham (2016). doi:\n10.1007\/978-3-319-40229-1_20"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"MJC Gordon","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979). doi:\n10.1007\/3-540-09724-4"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-662-48899-7_24","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L Hadarean","year":"2015","unstructured":"Hadarean, L., Barrett, C., Reynolds, A., Tinelli, C., Deters, M.: Fine grained SMT proofs for the theory of fixed-width bit-vectors. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 340\u2013355. Springer, Heidelberg (2015). doi:\n10.1007\/978-3-662-48899-7_24"},{"key":"25_CR13","unstructured":"Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. In: LICS 1987, pp. 194\u2013204. IEEE Computer Society (1987)"},{"key":"25_CR14","doi-asserted-by":"publisher","unstructured":"Katz, G., Barrett, C.W., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for DPLL(T)-based SMT solvers. In: Piskac, R., Talupur, M. (eds.) FMCAD 2016, pp. 93\u2013100. IEEE Computer Society (2016). doi:\n10.1109\/FMCAD.2016.7886666","DOI":"10.1109\/FMCAD.2016.7886666"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-39799-8_1"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1007\/978-3-540-78800-3_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Moskal","year":"2008","unstructured":"Moskal, M.: Rocket-fast proof checking for SMT solvers. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 486\u2013500. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-78800-3_38"},{"key":"25_CR17","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Proofs and refutations, and Z3. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) LPAR 2008 Workshops. CEUR Workshop Proceedings, vol. 418 (2008). \nCEUR-WS.org"},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-45949-9"},{"issue":"1\u20132","key":"25_CR19","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.ic.2004.10.011","volume":"199","author":"H Nivelle de","year":"2005","unstructured":"de Nivelle, H.: Translation of resolution proofs into short first-order proofs without choice axioms. Inf. Comput. 199(1\u20132), 24\u201354 (2005). doi:\n10.1016\/j.ic.2004.10.011","journal-title":"Inf. Comput."},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 335\u2013367. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-540-74591-4_18","volume-title":"TPHOLs 2007","author":"LC Paulson","year":"2007","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactivetheorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 232\u2013245. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-74591-4_18"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E\u00a01.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-45221-5_49"},{"key":"25_CR23","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/j.entcs.2008.12.121","volume":"228","author":"A Stump","year":"2009","unstructured":"Stump, A.: Proof checking technology for satisfiability modulo theories. Electr. Notes Theor. Comput. Sci. 228, 121\u2013133 (2009). doi:\n10.1016\/j.entcs.2008.12.121","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"25_CR24","unstructured":"Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP data-exchange formats for automated theorem proving tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems. Frontiers in Artificial Intelligence and Applications, vol. 112, pp. 201\u2013215. IOS Press (2004)"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-02959-2_10"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T09:40:39Z","timestamp":1499679639000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}