Find Research outputs

Search results

• 2020

  A Comprehensive Framework for Saturation Theorem Proving

  Waldmann, U., Tourret, S., Robillard, S. & Blanchette, J., 2020, Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I. Peltier, N. & Sofronie-Stokkermans, V. (eds.). Springer, Vol. 1. p. 316-334 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12166 LNAI).

  Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

  • Theorem proving
  • Theorem Proving
  • Saturation
  • Redundancy
  • Completeness

• 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 Journal › Article › Academic › peer-review

  Open Access

  File

  • Theorem proving
  28 Downloads (Pure)

• 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 26 p.

  Research output: Contribution to Journal › Article › Academic › peer-review

  • Surface mount technology
  • Data structures
  • Set theory
• 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 Journal › Article › Academic › peer-review

  Open Access

  • Functional programming
  • Computer programming languages
  • Data structures
  • Concretes
  • Experiments

• A verified SAT solver with watched literals using Imperative HOL

  Fleury, M., Blanchette, J. C. & Lammich, P., Jan 2018, CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018. New York, NY: Association for Computing Machinery, Inc, p. 158-171 14 p.

  Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

  • Data structures

• Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

  Schlichtkrull, A., Blanchette, J. C., Traytel, D. & Waldmann, U., 2018, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, p. 89-107 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI).

  Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

  • Theorem proving
  • Infrastructure
  • Automated Reasoning
  • Formal Proof
  • Theorem Proving

• Introduction to Milestones in Interactive Theorem Proving

  Avigad, J., Blanchette, J. C., Klein, G., Paulson, L., Popescu, A. & Snelting, G., Jun 2018, In : Journal of Automated Reasoning. 61, p. 1-8 8 p.

  Research output: Contribution to Journal › Editorial › Academic › peer-review

  Open Access

  File
  16 Downloads (Pure)

• Superposition for Lambda-Free Higher-Order Logic

  Bentkamp, A., Blanchette, J. C., Cruanes, S. & Waldmann, U., 2018, Automated Reasoning: 9th International Joint Conference, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 Oxford, UK, July 14–17, 2018 Proceedings. Galmiche, D., Schulz, S. & Sebastiani, R. (eds.). Springer/Verlag, p. 28-46 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI).

  Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

  • Higher-order Logic
  • Equivalence classes
  • Superposition
  • Calculus
  • Higher Order

• Superposition with Datatypes and Codatatypes

  Blanchette, J. C., Peltier, N. & Robillard, S., 2018, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, p. 370-387 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI).

  Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

  • Superposition
  • Axiom
  • Extension Theory
  • Acyclicity
  • First-order
• 2016

  A Decision Procedure for (Co)datatypes in SMT Solvers

  Reynolds, A. & Blanchette, J. C., 2016, Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence: IJCAI 2016, New York, NY, USA, 9-15 July 2016. IJCAI/AAAI Press, p. 4205-4209

  Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

  Open Access

  File
  10 Downloads (Pure)

• 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 Journal › Article › Academic › peer-review

  Open Access

  File

  • Syntactics
  • Machine learning
  • Servers
  98 Downloads (Pure)

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

  Blanchette, J. C., Fleury, M. & Weidenbach, C., 2016, Automated Reasoning - 8th International Joint Conference: IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. Springer, p. 25-44 (Lecture Notes in Computer Science; vol. 9706).

  Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

  Open Access

  File

  • Functional programming
  • Computer programming languages
  • Experiments
  97 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 Journal › Article › Academic › peer-review

  Open Access

  File
  7 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 Journal › Article › Academic › peer-review

  Open Access

  File

  • Hammers
  • Heuristic methods
  • Formal Proof
  • Libraries
  • Proof Search
  116 Downloads (Pure)

• Model Finding for Recursive Functions in SMT

  Reynolds, A., Blanchette, J. C., Cruanes, S. & Tinelli, C., 2016, Automated Reasoning - 8th International Joint Conference: IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. Springer, p. 133-151

  Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

  Open Access

  File

  • Recursive functions
  • Surface mount technology
  4 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 Journal › Article › Academic › peer-review

  Open Access

  File
  12 Downloads (Pure)