dr. Jasmin Christian Blanchette

    20162020

    Research output per year

    If you made any changes in Pure these will be visible here soon.

    Research Output

    Filter
    Article
    2020

    Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

    Schlichtkrull, A., Blanchette, J., Traytel, D. & Waldmann, U., Oct 2020, In : Journal of Automated Reasoning. 64, 7, p. 1169-1195 27 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Scalable Fine-Grained Proofs for Formula Processing

    Barbosa, H., Blanchette, J. C., Fleury, M. & Fontaine, P., Mar 2020, In : Journal of Automated Reasoning. 64, 3, p. 485-510

    Research output: Contribution to JournalArticleAcademicpeer-review

    2019

    A Formal Proof of the Expressiveness of Deep Learning

    Bentkamp, A., Blanchette, J. C. & Klakow, D., Aug 2019, In : Journal of Automated Reasoning. 63, 2, p. 347-368 22 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access

    Scalable Fine-Grained Proofs for Formula Processing

    Barbosa, H., Blanchette, J. C., Fleury, M. & Fontaine, P., 4 Jan 2019, In : Journal of Automated Reasoning. 64, 3, p. 1-26 26 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    2018

    A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

    Blanchette, J. C., Fleury, M., Lammich, P. & Weidenbach, C., 12 Mar 2018, In : Journal of Automated Reasoning. 2018, 1-4, p. 1-33 33 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access
    2017

    Language and Proofs for Higher-Order SMT (Work in Progress)

    Barbosa, H., Blanchette, J. C., Cruanes, S., El Ouraoui, D. & Fontaine, P., 2017, In : Electronic Proceedings in Theoretical Computer Science. 262, 262, p. 15-22 8 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access

    Soundness and Completeness Proofs by Coinductive Methods

    Blanchette, J. C., Popescu, A. & Traytel, D., Jan 2017, In : Journal of Automated Reasoning. 58, 1, p. 149-179 31 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    2016

    A Learning-Based Fact Selector for Isabelle/HOL

    Blanchette, J. C., Greenaway, D., Kaliszyk, C., Kühlwein, D. & Urban, J., 1 Oct 2016, In : Journal of Automated Reasoning. 57, 3, p. 219-244 26 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access
    File
    90 Downloads (Pure)

    Encoding Monomorphic and Polymorphic Types

    Blanchette, J. C., Böhme, S., Popescu, A. & Smallbone, N., 2016, In : Logical Methods in Computer Science.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access
    File
    6 Downloads (Pure)

    Hammering towards QED

    Blanchette, J. C., Kaliszyk, C., Paulson, L. C. & Urban, J., 2016, In : Journal of Formalized Reasoning. 9, 1, p. 101-148

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access
    File
    57 Downloads (Pure)

    Semi-intelligible Isar Proofs from Machine-Generated Proofs

    Blanchette, J. C., Böhme, S., Fleury, M., Smolka, S. J. & Steckermeier, A., 2016, In : Journal of Automated Reasoning. p. 155-200

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access
    File
    10 Downloads (Pure)