{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T07:19:58Z","timestamp":1742800798058},"reference-count":25,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2012,9,1]],"date-time":"2012-09-01T00:00:00Z","timestamp":1346457600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":331,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2012,9]]},"DOI":"10.1016\/j.entcs.2012.08.016","type":"journal-article","created":{"date-parts":[[2012,9,28]],"date-time":"2012-09-28T00:13:22Z","timestamp":1348791202000},"page":"243-256","source":"Crossref","is-referenced-by-count":1,"special_numbering":"C","title":["Extracting a DPLL Algorithm"],"prefix":"10.1016","volume":"286","author":[{"given":"Andrew","family":"Lawrence","sequence":"first","affiliation":[]},{"given":"Ulrich","family":"Berger","sequence":"additional","affiliation":[]},{"given":"Monika","family":"Seisenberger","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.entcs.2012.08.016_br0010","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.tcs.2003.10.023","article-title":"An arithmetic for non-size-increasing polynomial-time computation","volume":"318","author":"Aehlig","year":"2004","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.entcs.2012.08.016_br0020","series-title":"Automated Deduction \u2013 A Basis for Applications II","article-title":"Proof theory at work: Program development in the Minlog system","author":"Benl","year":"1998"},{"key":"10.1016\/j.entcs.2012.08.016_br0030","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/s11225-006-6604-5","article-title":"Program extraction from normalization proofs","volume":"82","author":"Berger","year":"2006","journal-title":"Studia Logica"},{"key":"10.1016\/j.entcs.2012.08.016_br0040","series-title":"CALCO 2011","first-page":"393","article-title":"Minlog \u2013 A Tool for Program Extraction Supporting Algebras and Coalgebras","volume":"vol. 6859","author":"Berger","year":"2011"},{"key":"10.1016\/j.entcs.2012.08.016_br0050","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1023\/A:1026748613865","article-title":"The Warshall algorithm and Dickson\u02bcs lemma: Two examples of realistic program extraction","volume":"26","author":"Berger","year":"2001","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/j.entcs.2012.08.016_br0060","article-title":"Interactive Theorem Proving and Program Development: Coq\u02bcArt: The Calculus of Inductive Constructions","author":"Bertot","year":"2004"},{"key":"10.1016\/j.entcs.2012.08.016_br0070","article-title":"Handbook of Satisfiability","volume":"vol. 185","author":"Biere","year":"2009"},{"key":"10.1016\/j.entcs.2012.08.016_br0080","series-title":"Automated Reasoning","first-page":"107","article-title":"Sledgehammer: Judgement day","volume":"vol. 6173","author":"B\u00f6hme","year":"2010"},{"key":"10.1016\/j.entcs.2012.08.016_br0090","series-title":"Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics","article-title":"A brief overview of Agda \u2014 A Functional Language with Dependent Types","volume":"vol. 5674","author":"Bove","year":"2009"},{"key":"10.1016\/j.entcs.2012.08.016_br0100","series-title":"Implementing Mathematics with the Nuprl Development System","author":"Constable","year":"1986"},{"key":"10.1016\/j.entcs.2012.08.016_br0110","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","article-title":"The relative efficiency of propositional proof systems","volume":"44","author":"Cook","year":"1979","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/j.entcs.2012.08.016_br0120","article-title":"Combinatory Logic","volume":"1","author":"Curry","year":"1958","journal-title":"Studies in Logic and the Foundations of Mathematics"},{"key":"10.1016\/j.entcs.2012.08.016_br0130","unstructured":"Howard, W.A., The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (1980)."},{"key":"10.1016\/j.entcs.2012.08.016_br0140","series-title":"Constructivity in Mathematics","first-page":"101","article-title":"Interpretation of analysis by means of constructive functionals of finite types","author":"Kreisel","year":"1959"},{"key":"10.1016\/j.entcs.2012.08.016_br0150","series-title":"Theorem Proving in Higher Order Logics","article-title":"A Reflexive Formalization of a SAT Solver in Coq","volume":"vol. 5170","author":"Lescuyer","year":"2008"},{"key":"10.1016\/j.entcs.2012.08.016_br0160","doi-asserted-by":"crossref","first-page":"57","DOI":"10.15388\/Informatica.2010.273","article-title":"Formal correctness proof for DPLL procedure","volume":"21","author":"Mari\u0107","year":"2010","journal-title":"Informatica"},{"key":"10.1016\/j.entcs.2012.08.016_br0170","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","article-title":"GRASP: A Search Algorithm for Propositional Satisfiability","volume":"48","author":"Marques-Silva","year":"1999","journal-title":"IEEE Trans. Computers"},{"key":"10.1016\/j.entcs.2012.08.016_br0180","first-page":"130","article-title":"Epigram: Practical Programming with Dependent Types","volume":"vol. 3622","author":"McBride","year":"2004"},{"key":"10.1016\/j.entcs.2012.08.016_br0190","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., C.F. Madigan, Y. Zhao, L. Zhang and S. Malik, Chaff: Engineering an efficient SAT solver, in: Annual ACM IEEE Design Automation Conference (2001), pp. 530\u2013535.","DOI":"10.1145\/378239.379017"},{"key":"10.1016\/j.entcs.2012.08.016_br0210","article-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","volume":"vol. 2283","author":"Nipkow","year":"1999"},{"key":"10.1016\/j.entcs.2012.08.016_br0220","article-title":"Isabelle: A Generic Theorem Prover","volume":"vol. 828","author":"Paulson","year":"1994"},{"key":"10.1016\/j.entcs.2012.08.016_br0230","unstructured":"Paulson, L.C. and K.W. Susanto, Source-Level Proof Reconstruction for Interactive Theorem Proving, in: Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u02bc07 (2007), pp. 232\u2013245."},{"key":"10.1016\/j.entcs.2012.08.016_br0240","series-title":"Proofs, Categories and Computations. Essays in honor of Grigori Mints","first-page":"171","article-title":"Decorating proofs","author":"Ratiu","year":"2010"},{"key":"10.1016\/j.entcs.2012.08.016_br0250","series-title":"Proofs and Computations","author":"Schwichtenberg","year":"2012"},{"key":"10.1016\/j.entcs.2012.08.016_br0260","series-title":"ASIAN","first-page":"162","article-title":"Reflecting BDDs in Coq","volume":"vol. 1961","author":"Verma","year":"2000"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066112000461?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066112000461?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T07:26:09Z","timestamp":1594711569000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066112000461"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9]]},"references-count":25,"alternative-id":["S1571066112000461"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2012.08.016","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2012,9]]}}}