{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:09:42Z","timestamp":1725538182050},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642042218"},{"type":"electronic","value":"9783642042225"}],"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-04222-5_18","type":"book-chapter","created":{"date-parts":[[2009,9,16]],"date-time":"2009-09-16T12:42:11Z","timestamp":1253104931000},"page":"287-303","source":"Crossref","is-referenced-by-count":5,"title":["Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme"],"prefix":"10.1007","author":[{"given":"St\u00e9phane","family":"Lescuyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sylvain","family":"Conchon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"18_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1023\/A:1021939521172","volume":"29","author":"M. Bezem","year":"2002","unstructured":"Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. JAR\u00a029(3), 253\u2013275 (2002)","journal-title":"JAR"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","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, vol.\u00a04790, pp. 151\u2013165. Springer, Heidelberg (2007)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software","author":"S. Boutin","year":"1997","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol.\u00a01281, pp. 515\u2013529. Springer, Heidelberg (1997)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/10930755_18","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Chrz\u0105szcz","year":"2003","unstructured":"Chrz\u0105szcz, J.: Implementation of modules in the Coq system. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 270\u2013286. Springer, Heidelberg (2003)"},{"key":"18_CR5","unstructured":"Conchon, S., Contejean, E.: The Alt-Ergo Prover, http:\/\/alt-ergo.lri.fr\/"},{"key":"18_CR6","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/11532231_2","volume-title":"Automated Deduction \u2013 CADE-20","author":"E. Contejean","year":"2005","unstructured":"Contejean, E., Corbineau, P.: Reflecting Proofs in First-Order Logic with Equality. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 7\u201322. Springer, Heidelberg (2005)"},{"key":"18_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-74621-8_10","volume-title":"Frontiers of Combining Systems","author":"E. Contejean","year":"2007","unstructured":"Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Certification of automated termination proofs. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 148\u2013162. Springer, Heidelberg (2007)"},{"key":"18_CR8","unstructured":"The Coq Proof Assistant, http:\/\/coq.inria.fr\/"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-74464-1_6","volume-title":"Types for Proofs and Programs","author":"P. Corbineau","year":"2007","unstructured":"Corbineau, P.: Deciding equality in the constructor theory. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 78\u201392. Springer, Heidelberg (2007)"},{"issue":"7","key":"18_CR10","doi-asserted-by":"publisher","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. Communication of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communication of the ACM"},{"issue":"3","key":"18_CR11","doi-asserted-by":"publisher","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\u00a07(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"18_CR12","series-title":"LNAI","first-page":"558","volume-title":"CADE-10 1990","author":"T.B. Tour de la","year":"1990","unstructured":"de la Tour, T.B.: Minimizing the number of clauses by renaming. In: Stickel, M.E. (ed.) CADE-10 1990. LNCS (LNAI), vol.\u00a0449, pp. 558\u2013572. Springer, Heidelberg (1990)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L.M. Moura de","year":"2007","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"18_CR14","volume-title":"JFLA, Pontarlier (France)","author":"D. Delahaye","year":"2001","unstructured":"Delahaye, D., Mayero, M.: Field: une proc\u00e9dure de d\u00e9cision pour les nombres r\u00e9els en Coq. In: JFLA, Pontarlier (France), INRIA, Janvier (2001)"},{"issue":"3","key":"18_CR15","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"issue":"3","key":"18_CR16","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. J. Symb. Log.\u00a057(3), 795\u2013807 (1992)","journal-title":"J. Symb. Log."},{"key":"18_CR17","unstructured":"Dyckhoff, R.: Some benchmark formulae for intuitionistic propositional logic (1997)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"18_CR19","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/1159876.1159880","volume-title":"ML","author":"J.-C. Filli\u00e2tre","year":"2006","unstructured":"Filli\u00e2tre, J.-C., Conchon, S.: Type-safe modular hash-consing. In: Kennedy, A., Pottier, F. (eds.) ML, pp. 12\u201319. ACM, New York (2006)"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 98\u2013113. Springer, Heidelberg (2005)"},{"key":"18_CR21","unstructured":"Lescuyer, S., Conchon, S.: A Reflexive Formalization of a SAT Solver in Coq. In: TPHOLS 2008 Emerging Trends (2008)"},{"issue":"10","key":"18_CR22","doi-asserted-by":"publisher","first-page":"1575","DOI":"10.1016\/j.ic.2005.05.010","volume":"204","author":"J. Meng","year":"2006","unstructured":"Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: first prototype. Inf. Comput.\u00a0204(10), 1575\u20131596 (2006)","journal-title":"Inf. Comput."},{"key":"18_CR23","first-page":"530","volume-title":"DAC 2001","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: DAC 2001, pp. 530\u2013535. ACM Press, New York (2001)"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BFb0054274","volume-title":"Automated Deduction - CADE-15","author":"A. Nonnengart","year":"1998","unstructured":"Nonnengart, A., Rock, G., Weidenbach, C.: On generating small clause normal forms. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS, vol.\u00a01421, pp. 397\u2013411. Springer, Heidelberg (1998)"},{"issue":"3","key":"18_CR25","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput.\u00a02(3), 293\u2013304 (1986)","journal-title":"J. Symb. Comput."},{"key":"18_CR26","first-page":"4","volume":"8","author":"W. Pugh","year":"1992","unstructured":"Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM\u00a08, 4\u201313 (1992)","journal-title":"Communications of the ACM"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivations in the propositional calculus, Part II. Studies in Mathematics and Mathematical Logic, pp. 115\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"18_CR28","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.jal.2007.07.003","volume":"7","author":"T. Weber","year":"2009","unstructured":"Weber, T., Amjad, H.: Efficiently Checking Propositional Refutations in HOL Theorem Provers. Journal of Applied Logic\u00a07, 26\u201340 (2009)","journal-title":"Journal of Applied Logic"}],"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-642-04222-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T13:17:33Z","timestamp":1558531053000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04222-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642042218","9783642042225"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04222-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}