Find Research Outputs

Search results

• Conference contribution

  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

• 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 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
  96 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)
• Article

  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
  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)

• 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
  13 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
  102 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

• 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)