Researcher Portfolio

 
   

Blanchette, Jasmin

Automation of Logic, MPI for Informatics, Max Planck Society  

 

Researcher Profile

 
Position: Automation of Logic, MPI for Informatics, Max Planck Society
Researcher ID: https://pure.mpg.de/cone/persons/resource/persons183227

External references

 

Publications

 
  (1 - 25 of 65)
 : Desharnais, M., Toth, B., Waldmann, U., Blanchette, J., & Tourret, S. (2024). A Modular Formalization of Superposition in Isabelle/HOL. In Y. Bertot, T. Kutsia, & M. Norrish (Eds.), 15th International Conference on Interactive Theorem Proving (pp. 1-20). Wadern: Schloss Dagstuhl. doi:10.4230/LIPIcs.ITP.2024.12. [PubMan] : Blanchette, J., & Vukmirović, P. (2023). SAT-Inspired Higher-Order Eliminations. Logical Methods in Computer Science, 19(2): 9, pp. 1-23. doi:10.46298/lmcs-19(2:9)2023. [PubMan] : Blanchette, J., Qiu, Q., & Tourret, S. (2023). Given Clause Loops. Archive of Formal Proofs. Retrieved from https://isa-afp.org/entries/Given_Clause_Loops.html. [PubMan] : Ebner, G., Blanchette, J., & Tourret, S. (2023). Unifying Splitting. Journal of Automated Reasoning, 67(2): 16, pp. 1-44. doi:10.1007/s10817-023-09660-8. [PubMan] : Blanchette, J., Qiu, Q., & Tourret, S. (2023). Verified Given Clause Procedures. In B. Pientka, & C. Tinelli (Eds.), Automated Deductions -- CADE 29 (pp. 61-77). Berlin: Springer. [PubMan] : Bentkamp, A., Blanchette, J., Nummelin, V., Tourret, S., Vukmirović, P., & Waldmann, U. (2023). Mechanical Mathematicians. Communications of the ACM, 66(4), 80-90. doi:10.1145/3557998. [PubMan] : Bentkamp, A., Blanchette, J., Tourret, S., & Vukmirović, P. (2023). Superposition for Higher-Order Logic. Journal of Automated Reasoning, 67(1): 10. doi:10.1007/s10817-022-09649-9. [PubMan] : Bentkamp, A., Blanchette, J., Nummelin, V., Tourret, S., & Waldmann, U. (2023). Complete and Efficient Higher-Order Reasoning via Lambda-Superposition. ACM SIGLOG News, 10(4), 25-40. doi:10.1145/3636362.3636367. [PubMan] : Vukmirović, P., Blanchette, J., Cruanes, S., & Schulz, S. (2022). Extending a Brainiac Prover to Lambda-Free Higher-Order Logic. International Journal on Software Tools for Technology Transfer (STTT), 24, 67-87. doi:10.1007/s10009-021-00639-7. [PubMan] : Desharnais, M., Vukmirović, P., Blanchette, J., & Wenzel, M. (2022). Seventeen Provers Under the Hammer. In J. Andronick, & L. de Moura (Eds.), 13th International Conference on Interactive Theorem Proving (pp. 118-87). Wadern: Schloss Dagstuhl. doi:10.4230/LIPIcs.ITP.2022.8. [PubMan] : Waldmann, U., Tourret, S., Robillard, S., & Blanchette, J. (2022). A Comprehensive Framework for Saturation Theorem Proving. Journal of Automated Reasoning, 66, 499-539. doi:10.1007/s10817-022-09621-7. [PubMan] : Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., & Tourret, S. (2022). Making Higher-Order Superposition Work. Journal of Automated Reasoning, 66, 541-564. doi:10.1007/s10817-021-09613-z. [PubMan] : Tourret, S., & Blanchette, J. (2021). A Modular Isabelle Framework for Verifying Saturation Provers. In C. Hriţcu, & A. Popescu (Eds.), CPP '21 (pp. 224-237). New York, NY: ACM. doi:10.1145/3437992.3439912. [PubMan] : Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., & Tourret, S. (2021). Making Higher-Order Superposition Work. In A. Platzer, & G. Sutcliffe (Eds.), Automated Deduction - CADE 28 (pp. 415-432). Berlin: Springer. doi:10.1007/978-3-030-79876-5_24. [PubMan] : Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., & Waldmann, U. (2021). Superposition with Lambdas. Journal of Automated Reasoning, 65, 893-940. doi:10.1007/s10817-021-09595-y. [PubMan] : Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., & Waldmann, U. (2021). Superposition with Lambdas. Retrieved from https://arxiv.org/abs/2102.00453. [PubMan] : Ebner, G., Blanchette, J., & Tourret, S. (2021). A Unifying Splitting Framework. In A. Platzer, & G. Sutcliffe (Eds.), Automated Deduction - CADE 28 (pp. 344-360). Berlin: Springer. doi:10.1007/978-3-030-79876-5_20. [PubMan] : Bentkamp, A., Blanchette, J., Tourret, S., & Vukmirović, P. (2021). Superposition for Full Higher-order Logic. In A. Platzer, & G. Sutcliffe (Eds.), Automated Deduction - CADE 28 (pp. 396-412). Berlin: Springer. doi:10.1007/978-3-030-79876-5_23. [PubMan] : Bentkamp, A., Blanchette, J., Cruanes, S., & Waldmann, U. (2021). Superposition for Lambda-Free Higher-Order Logic. Logical Methods in Computer Science, 17(2): 1, pp. 1-38. doi:10.23638/LMCS-17(2:1)2021. [PubMan] : Blanchette, J., & Hriţcu, C. (Eds.). (2020). CPP '20. New York, NY: ACM. doi:10.1145/3372885. [PubMan] : Bentkamp, A., Blanchette, J., Cruanes, S., & Waldmann, U. (2020). Superposition for Lambda-Free Higher-Order Logic. Retrieved from https://arxiv.org/abs/2005.02094. [PubMan] : Schlichtkrull, A., Blanchette, J., Traytel, D., & Waldmann, U. (2020). Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. Journal of Automated Reasoning, 64, 1169-1195. doi:10.1007/s10817-020-09561-0. [PubMan] : Barbosa, H., Blanchette, J. C., & Fontaine, P. (2020). Scalable Fine-Grained Proofs for Formula Processing. Journal of Automated Reasoning, 64(3), 485-510. doi:10.1007/s10817-018-09502-y. [PubMan] : Waldmann, U., Tourret, S., Robillard, S., & Blanchette, J. (2020). A Comprehensive Framework for Saturation Theorem Proving. In N. Peltier, & V. Sofronie-Stokkermans (Eds.), Automated Reasoning (pp. 316-334). Berlin: Springer. doi:10.1007/978-3-030-51074-9_18. [PubMan] : Vukmirović, P., Blanchette, J. C., Cruanes, S., & Schulz, S. (2019). Extending a Brainiac Prover to Lambda-Free Higher-Order Logic. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 192-210). New York, NY: Springer. doi:10.1007/978-3-030-17462-0_11. [PubMan]