关注
Jasmin Blanchette
Jasmin Blanchette
在 ifi.lmu.de 的电子邮件经过验证 - 首页
标题
引用次数
引用次数
年份
C++ GUI Programming with Qt 4
J Blanchette, M Summerfield
Pearson Education, 2008
1319*2008
Nitpick: A counterexample generator for higher-order logic based on a relational model finder
JC Blanchette, T Nipkow
International conference on interactive theorem proving, 131-146, 2010
3452010
Extending Sledgehammer with SMT solvers
JC Blanchette, S Böhme, LC Paulson
Journal of automated reasoning 51 (1), 109-128, 2013
3092013
Hammering towards QED
JC Blanchette, C Kaliszyk, LC Paulson, J Urban
Journal of Formalized Reasoning 9 (1), 101-148, 2016
2192016
Automatic proof and disproof in Isabelle/HOL
JC Blanchette, L Bulwahn, T Nipkow
Frontiers of Combining Systems: 8th International Symposium, FroCoS 2011 …, 2011
1362011
Truly modular (co)datatypes for Isabelle/HOL
JC Blanchette, J Hölzl, A Lochbihler, L Panny, A Popescu, D Traytel
Interactive Theorem Proving, 93-110, 2014
1242014
MaSh: Machine learning for Sledgehammer
D Kühlwein, JC Blanchette, C Kaliszyk, J Urban
International Conference on Interactive Theorem Proving, 35-50, 2013
1082013
Encoding monomorphic and polymorphic types
JC Blanchette, S Böhme, A Popescu, N Smallbone
Logical Methods in Computer Science 12, 2017
95*2017
TFF1: The TPTP typed first-order form with rank-1 polymorphism
JC Blanchette, A Paskevich
Automated Deduction–CADE-24: 24th International Conference on Automated …, 2013
842013
A verified SAT solver framework with learn, forget, restart, and incrementality
JC Blanchette, M Fleury, P Lammich, C Weidenbach
Journal of automated reasoning 61, 333-365, 2018
812018
Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving
D Traytel, A Popescu, JC Blanchette
Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer …, 2012
802012
A learning-based fact selector for Isabelle/HOL
JC Blanchette, D Greenaway, C Kaliszyk, D Kühlwein, J Urban
Journal of Automated Reasoning 57, 219-244, 2016
792016
Mining the Archive of Formal Proofs
JC Blanchette, M Haslbeck, D Matichuk, T Nipkow
Intelligent Computer Mathematics, 3-17, 2015
632015
Superposition for lambda-free higher-order logic
A Bentkamp, J Blanchette, S Cruanes, U Waldmann
Logical Methods in Computer Science 17, 2021
552021
A decision procedure for (co)datatypes in SMT solvers
A Reynolds, JC Blanchette
Automated Deduction-CADE-25, 197-213, 2015
552015
Superposition with lambdas
A Bentkamp, J Blanchette, S Tourret, P Vukmirović, U Waldmann
Journal of Automated Reasoning 65 (7), 893-940, 2021
542021
Extending a brainiac prover to lambda-free higher-order logic
P Vukmirović, JC Blanchette, S Cruanes, S Schulz
International Conference on Tools and Algorithms for the Construction and …, 2019
522019
More SPASS with Isabelle: Superposition with hard sorts and configurable simplification
JC Blanchette, A Popescu, D Wand, C Weidenbach
Interactive Theorem Proving, 345-360, 2012
502012
Scalable fine-grained proofs for formula processing
H Barbosa, JC Blanchette, P Fontaine
CADE, 2017
442017
A comprehensive framework for saturation theorem proving
U Waldmann, S Tourret, S Robillard, J Blanchette
IJCAR, 2020
432020
系统目前无法执行此操作,请稍后再试。
文章 1–20