Marić, Filip Formalization and implementation of modern SAT solvers. (English) Zbl 1187.68557 J. Autom. Reasoning 43, No. 1, 81-119 (2009). MSC: 68T20 68T15 68Q60 PDF BibTeX XML Cite \textit{F. Marić}, J. Autom. Reasoning 43, No. 1, 81--119 (2009; Zbl 1187.68557) Full Text: DOI
Monroy, Raúl; Bundy, Alan; Green, Ian On process equivalence = equation solving in CCS. (English) Zbl 1191.68443 J. Autom. Reasoning 43, No. 1, 53-80 (2009). MSC: 68Q85 PDF BibTeX XML Cite \textit{R. Monroy} et al., J. Autom. Reasoning 43, No. 1, 53--80 (2009; Zbl 1191.68443) Full Text: DOI
Dufourd, Jean-François An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps. (English) Zbl 1187.68525 J. Autom. Reasoning 43, No. 1, 19-51 (2009). MSC: 68T15 03B35 PDF BibTeX XML Cite \textit{J.-F. Dufourd}, J. Autom. Reasoning 43, No. 1, 19--51 (2009; Zbl 1187.68525) Full Text: DOI
Blanchette, Jasmin Christian Proof pearl: Mechanizing the textbook proof of Huffman’s algorithm. (English) Zbl 1187.68523 J. Autom. Reasoning 43, No. 1, 1-18 (2009). MSC: 68T15 PDF BibTeX XML Cite \textit{J. C. Blanchette}, J. Autom. Reasoning 43, No. 1, 1--18 (2009; Zbl 1187.68523) Full Text: DOI