Author:Jasmin Christian Blanchette

Publications
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann EasyChair Preprint 396
PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving Jasmin Christian Blanchette and Josef Urban (editors) EPiC Series in Computing, volume 14
Towards Strong Higher-Order Automation for Fast Interactive Verification Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz and Uwe Waldmann In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
My Life with an Automatic Theorem Prover Jasmin Christian Blanchette In:Proceedings of the 1st and 2nd Vampire Workshops
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs Steffen Juilf Smolka and Jasmin Christian Blanchette In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Redirecting Proofs by Contradiction Jasmin Christian Blanchette In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod Jasmin Christian Blanchette In:LPAR-17-short. short papers for 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning.
Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers Lawrence C. Paulson and Jasmin Christian Blanchette In:IWIL 2010. The 8th International Workshop on the Implementation of Logics

Keyphrases

automatic theorem provers⁴, completeness, counterexample generation, direct proofs, first-order logic, higher-order logic³, interactive theorem proving, Isabelle/HOL⁴, model finding, proof assistant, proof assistants³, prover, resolution², Satisfiability Modulo Theories (SMT), simple type theory, Skolemization, Sledgehammer², structured proofs, superposition calculus, Vampire.