×

Blanchette, Jasmin Christian

Author ID: blanchette.jasmin-christian Recent zbMATH articles by "Blanchette, Jasmin Christian"
Published as: Blanchette, Jasmin Christian; Blanchette, Jasmin; Blanchette, Jasmin C.

Publications by Year

Citations contained in zbMATH Open

54 Publications have been cited 600 times in 295 Documents Cited by Year
Nitpick: a counterexample generator for higher-order logic based on a relational model finder. Zbl 1291.68326
Blanchette, Jasmin Christian; Nipkow, Tobias
61
2010
Extending Sledgehammer with SMT solvers. Zbl 1314.68272
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.
41
2013
Hammering towards QED. Zbl 1451.68318
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef
35
2016
Truly modular (co)datatypes for Isabelle/HOL. Zbl 1416.68151
Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy
35
2014
Extending Sledgehammer with SMT solvers. Zbl 1314.68271
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.
27
2011
Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214
Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias
26
2011
A comprehensive framework for saturation theorem proving. Zbl 1512.68433
Waldmann, Uwe; Tourret, Sophie; Robillard, Simon; Blanchette, Jasmin
21
2020
Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. Zbl 1362.68251
Traytel, Dmitry; Popescu, Andrei; Blanchette, Jasmin C.
19
2012
TFF1: the TPTP typed first-order form with rank-1 polymorphism. Zbl 1381.68260
Blanchette, Jasmin Christian; Paskevich, Andrei
17
2013
Encoding monomorphic and polymorphic types. Zbl 1381.68259
Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas
16
2013
MaSh: machine learning for Sledgehammer. Zbl 1317.68215
Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef
16
2013
A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149
Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef
16
2016
Semi-intelligible Isar proofs from machine-generated proofs. Zbl 1356.68178
Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert
13
2016
Foundational extensible corecursion: a proof assistant perspective. Zbl 1360.68358
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy
13
2015
Friends with benefits. Implementing corecursion in foundational proof assistants. Zbl 1485.68280
Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy
13
2017
Superposition with lambdas. Zbl 1471.03014
Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe
13
2019
Unified classical logic completeness. A coinductive pearl. Zbl 1409.68250
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy
12
2014
Superposition for full higher-order logic. Zbl 1497.03030
Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar
12
2021
Superposition for \(\lambda\)-free higher-order logic. Zbl 1511.68302
Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe
12
2018
Mining the Archive of Formal Proofs. Zbl 1417.68176
Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias
11
2015
Cardinals in Isabelle/HOL. Zbl 1416.68152
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy
10
2014
Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68306
Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe
10
2018
Soundness and completeness proofs by coinductive methods. Zbl 1409.68251
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy
9
2017
A transfinite Knuth-Bendix order for lambda-free higher-order terms. Zbl 1496.03037
Becker, Heiko; Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel
9
2017
Making higher-order superposition work. Zbl 1512.68431
Vukmirović, Petar; Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Nummelin, Visa; Tourret, Sophie
9
2021
A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1475.68432
Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph
8
2016
LEO-II and Satallax on the Sledgehammer test bench. Zbl 1262.68161
Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C.
8
2013
More SPASS with Isabelle. Superposition with hard sorts and configurable simplification. Zbl 1360.68742
Blanchette, Jasmin Christian; Popescu, Andrei; Wand, Daniel; Weidenbach, Christoph
8
2012
Superposition with lambdas. Zbl 07433023
Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe
7
2021
Mechanizing the metatheory of Sledgehammer. Zbl 1398.68479
Blanchette, Jasmin Christian; Popescu, Andrei
7
2013
A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1448.68457
Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph
7
2018
Encoding monomorphic and polymorphic types. Zbl 1445.68327
Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas
6
2016
Superposition for lambda-free higher-order logic. Zbl 07350767
Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe
6
2021
Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 1495.68238
Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy
6
2017
A lambda-free higher-order recursive path order. Zbl 1486.68085
Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel
5
2017
A decision procedure for (co)datatypes in SMT solvers. Zbl 1410.68337
Reynolds, Andrew; Blanchette, Jasmin Christian
5
2017
Scalable fine-grained proofs for formula processing. Zbl 1468.68278
Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal
5
2020
A unifying splitting framework. Zbl 07437088
Ebner, Gabriel; Blanchette, Jasmin; Tourret, Sophie
5
2021
Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68307
Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe
5
2020
Witnessing (co)datatypes. Zbl 1335.68224
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy
4
2015
A decision procedure for (co)datatypes in SMT solvers. Zbl 1465.68297
Reynolds, Andrew; Blanchette, Jasmin Christian
4
2015
Model finding for recursive functions in SMT. Zbl 1475.68448
Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare
4
2016
Foundational nonuniform (co)datatypes for higher-order logic. Zbl 1457.68173
Blanchette, Jasmin Christian; Meier, Fabian; Popescu, Andrei; Traytel, Dmitriy
4
2017
Monotonicity inference for higher-order formulas. Zbl 1291.03016
Blanchette, Jasmin Christian; Krauss, Alexander
3
2010
Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. Zbl 1434.03025
Blanchette, Jasmin Christian; Fleury, Mathias; Traytel, Dmitriy
3
2017
Superposition with datatypes and codatatypes. Zbl 1511.68304
Blanchette, Jasmin Christian; Peltier, Nicolas; Robillard, Simon
3
2018
SAT-inspired eliminations for superposition. Zbl 07650603
Vukmirović, Petar; Blanchette, Jasmin; Heule, Marijn J. H.
2
2023
Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Zbl 1343.68004
2
2016
Monotonicity inference for higher-order formulas. Zbl 1266.03021
Blanchette, Jasmin Christian; Krauss, Alexander
2
2011
Making higher-order superposition work. Zbl 1512.68432
Vukmirović, Petar; Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Nummelin, Visa; Tourret, Sophie
1
2022
Scalable fine-grained proofs for formula processing. Zbl 1494.68280
Barbosa, Haniel; Blanchette, Jasmin Christian; Fontaine, Pascal
1
2017
Tests and proofs. 9th international conference, TAP 2015, held as part of STAF 2015, L’Aquila, Italy, July 22–24, 2015. Proceedings. Zbl 1347.68005
1
2015
Introduction to “Milestones in interactive theorem proving”. Zbl 1398.00118
1
2018
A formal proof of the expressiveness of deep learning. Zbl 1468.68280
Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich
1
2017
SAT-inspired eliminations for superposition. Zbl 07650603
Vukmirović, Petar; Blanchette, Jasmin; Heule, Marijn J. H.
2
2023
Making higher-order superposition work. Zbl 1512.68432
Vukmirović, Petar; Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Nummelin, Visa; Tourret, Sophie
1
2022
Superposition for full higher-order logic. Zbl 1497.03030
Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar
12
2021
Making higher-order superposition work. Zbl 1512.68431
Vukmirović, Petar; Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Nummelin, Visa; Tourret, Sophie
9
2021
Superposition with lambdas. Zbl 07433023
Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe
7
2021
Superposition for lambda-free higher-order logic. Zbl 07350767
Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe
6
2021
A unifying splitting framework. Zbl 07437088
Ebner, Gabriel; Blanchette, Jasmin; Tourret, Sophie
5
2021
A comprehensive framework for saturation theorem proving. Zbl 1512.68433
Waldmann, Uwe; Tourret, Sophie; Robillard, Simon; Blanchette, Jasmin
21
2020
Scalable fine-grained proofs for formula processing. Zbl 1468.68278
Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal
5
2020
Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68307
Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe
5
2020
Superposition with lambdas. Zbl 1471.03014
Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe
13
2019
Superposition for \(\lambda\)-free higher-order logic. Zbl 1511.68302
Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe
12
2018
Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68306
Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe
10
2018
A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1448.68457
Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph
7
2018
Superposition with datatypes and codatatypes. Zbl 1511.68304
Blanchette, Jasmin Christian; Peltier, Nicolas; Robillard, Simon
3
2018
Introduction to “Milestones in interactive theorem proving”. Zbl 1398.00118
1
2018
Friends with benefits. Implementing corecursion in foundational proof assistants. Zbl 1485.68280
Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy
13
2017
Soundness and completeness proofs by coinductive methods. Zbl 1409.68251
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy
9
2017
A transfinite Knuth-Bendix order for lambda-free higher-order terms. Zbl 1496.03037
Becker, Heiko; Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel
9
2017
Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 1495.68238
Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy
6
2017
A lambda-free higher-order recursive path order. Zbl 1486.68085
Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel
5
2017
A decision procedure for (co)datatypes in SMT solvers. Zbl 1410.68337
Reynolds, Andrew; Blanchette, Jasmin Christian
5
2017
Foundational nonuniform (co)datatypes for higher-order logic. Zbl 1457.68173
Blanchette, Jasmin Christian; Meier, Fabian; Popescu, Andrei; Traytel, Dmitriy
4
2017
Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. Zbl 1434.03025
Blanchette, Jasmin Christian; Fleury, Mathias; Traytel, Dmitriy
3
2017
Scalable fine-grained proofs for formula processing. Zbl 1494.68280
Barbosa, Haniel; Blanchette, Jasmin Christian; Fontaine, Pascal
1
2017
A formal proof of the expressiveness of deep learning. Zbl 1468.68280
Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich
1
2017
Hammering towards QED. Zbl 1451.68318
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef
35
2016
A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149
Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef
16
2016
Semi-intelligible Isar proofs from machine-generated proofs. Zbl 1356.68178
Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert
13
2016
A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1475.68432
Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph
8
2016
Encoding monomorphic and polymorphic types. Zbl 1445.68327
Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas
6
2016
Model finding for recursive functions in SMT. Zbl 1475.68448
Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare
4
2016
Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Zbl 1343.68004
2
2016
Foundational extensible corecursion: a proof assistant perspective. Zbl 1360.68358
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy
13
2015
Mining the Archive of Formal Proofs. Zbl 1417.68176
Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias
11
2015
Witnessing (co)datatypes. Zbl 1335.68224
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy
4
2015
A decision procedure for (co)datatypes in SMT solvers. Zbl 1465.68297
Reynolds, Andrew; Blanchette, Jasmin Christian
4
2015
Tests and proofs. 9th international conference, TAP 2015, held as part of STAF 2015, L’Aquila, Italy, July 22–24, 2015. Proceedings. Zbl 1347.68005
1
2015
Truly modular (co)datatypes for Isabelle/HOL. Zbl 1416.68151
Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy
35
2014
Unified classical logic completeness. A coinductive pearl. Zbl 1409.68250
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy
12
2014
Cardinals in Isabelle/HOL. Zbl 1416.68152
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy
10
2014
Extending Sledgehammer with SMT solvers. Zbl 1314.68272
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.
41
2013
TFF1: the TPTP typed first-order form with rank-1 polymorphism. Zbl 1381.68260
Blanchette, Jasmin Christian; Paskevich, Andrei
17
2013
Encoding monomorphic and polymorphic types. Zbl 1381.68259
Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas
16
2013
MaSh: machine learning for Sledgehammer. Zbl 1317.68215
Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef
16
2013
LEO-II and Satallax on the Sledgehammer test bench. Zbl 1262.68161
Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C.
8
2013
Mechanizing the metatheory of Sledgehammer. Zbl 1398.68479
Blanchette, Jasmin Christian; Popescu, Andrei
7
2013
Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. Zbl 1362.68251
Traytel, Dmitry; Popescu, Andrei; Blanchette, Jasmin C.
19
2012
More SPASS with Isabelle. Superposition with hard sorts and configurable simplification. Zbl 1360.68742
Blanchette, Jasmin Christian; Popescu, Andrei; Wand, Daniel; Weidenbach, Christoph
8
2012
Extending Sledgehammer with SMT solvers. Zbl 1314.68271
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.
27
2011
Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214
Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias
26
2011
Monotonicity inference for higher-order formulas. Zbl 1266.03021
Blanchette, Jasmin Christian; Krauss, Alexander
2
2011
Nitpick: a counterexample generator for higher-order logic based on a relational model finder. Zbl 1291.68326
Blanchette, Jasmin Christian; Nipkow, Tobias
61
2010
Monotonicity inference for higher-order formulas. Zbl 1291.03016
Blanchette, Jasmin Christian; Krauss, Alexander
3
2010
all top 5

Cited by 370 Authors

35 Blanchette, Jasmin Christian
22 Kaliszyk, Cezary
22 Urban, Josef
18 Benzmüller, Christoph Ewald
13 Popescu, Andrei
12 Guttmann, Walter
12 Tourret, Sophie
11 Bentkamp, Alexander
11 Lochbihler, Andreas
11 Vukmirović, Petar
10 Paulson, Lawrence Charles
10 Reynolds, Andrew
9 Traytel, Dmitry
8 Barrett, Clark W.
8 Foster, Simon
8 Jakubův, Jan
8 Sutcliffe, Geoff
7 Tinelli, Cesare
7 Waldmann, Uwe
6 Cruanes, Simon
6 Fleury, Mathias
6 Steen, Alexander
6 Weidenbach, Christoph
5 Fuenmayor, David
5 Kunčar, Ondřej
5 Lammich, Peter
5 Nipkow, Tobias
5 Reger, Giles
5 Schlichtkrull, Anders
5 Woodcock, James C. P.
5 Zohar, Yoni
4 Abel, Andreas M.
4 Bhayat, Ahmed
4 Böhme, Sascha
4 Brown, Chad Edward
4 Gauthier, Thibault
4 Heule, Marijn J. H.
4 Niemetz, Aina
4 Norrish, Michael
4 Nummelin, Visa
4 Pąk, Karol
4 Preiner, Mathias
4 Struth, Georg
4 Suda, Martin
4 Vyskočil, Jiří
4 Zeyda, Frank
3 Avigad, Jeremy
3 Barbosa, Haniel
3 Bonacina, Maria Paola
3 Chvalovský, Karel
3 de Boer, Frank S.
3 De Gouw, Stijn
3 Desharnais, Martin
3 Divasón, Jose
3 Duarte, André
3 Dubois, Catherine
3 Färber, Michael
3 Fontaine, Pascal
3 From, Asta Halkjær
3 Grabowski, Adam
3 Janičić, Predrag
3 Korovin, Konstantin
3 Koutsoukou-Argyraki, Angeliki
3 Momigliano, Alberto
3 Narboux, Julien
3 Olšák, Miroslav
3 Pease, Alison
3 Rabe, Florian
3 Scott, Dana Stewart
3 Smallbone, Nicholas
3 Thiemann, René
3 Villadsen, Jørgen
3 Weber, Tjark
3 Yamada, Akihisa
2 Abdulaziz, Mohammad
2 Armstrong, Alasdair
2 Baek, Seulkee
2 Basold, Henning
2 Baumgartner, Peter
2 Beeson, Michael J.
2 Berghammer, Rudolf
2 Bian, Jinting
2 Brunner, Julian
2 Bundy, Alan
2 Bury, Guillaume
2 Cauderlier, Raphaël
2 Cavalcanti, Ana
2 Claessen, Koen
2 Czajka, Łukasz
2 Delahaye, David
2 Dubut, Jérémy
2 Ebner, Gabriel
2 Fleuriot, Jacques D.
2 Fürer, Basil
2 Gheri, Lorenzo
2 Giorgetti, Alain
2 Gretton, Charles
2 Grov, Gudmund
2 Guan, Yong
2 Halmagrand, Pierre
...and 270 more Authors

Citations by Year