Edit Profile (opens in new tab) Blanchette, Jasmin Christian Compute Distance To: Compute Author ID: blanchette.jasmin-christian Published as: Blanchette, Jasmin Christian; Blanchette, Jasmin; Blanchette, Jasmin C. more...less Documents Indexed: 56 Publications since 2009 5 Contributions as Editor Co-Authors: 57 Co-Authors with 60 Joint Publications 843 Co-Co-Authors all top 5 Co-Authors 1 single-authored 15 Popescu, Andrei 13 Traytel, Dmitry 10 Waldmann, Uwe 9 Bentkamp, Alexander 8 Tourret, Sophie 6 Fleury, Mathias 6 Vukmirović, Petar 5 Böhme, Sascha 5 Cruanes, Simon 5 Paulson, Lawrence Charles 3 Kaliszyk, Cezary 3 Kühlwein, Daniel 3 Lochbihler, Andreas 3 Nipkow, Tobias 3 Reynolds, Andrew 3 Robillard, Simon 3 Urban, Josef 3 Wand, Daniel 3 Weidenbach, Christoph 2 Barbosa, Haniel 2 Bouzy, Aymeric 2 Fontaine, Pascal 2 Hölzl, Johannes 2 Klakow, Dietrich 2 Krauss, Alexander 2 Meier, Fabian 2 Merz, Stephan 2 Nummelin, Visa 2 Panny, Lorenz 2 Schlichtkrull, Anders 2 Smallbone, Nicholas 1 Avigad, Jeremy 1 Becker, Heiko 1 Biendarra, Julian 1 Bulwahn, Lukas 1 Claessen, Koen 1 Desharnais, Martin 1 Ebner, Gabriel 1 Greenaway, David 1 Haslbeck, Maximilian P. L. 1 Heule, Marijn J. H. 1 Klein, Gerwin 1 Kosmatov, Nikolai 1 Kovács, Laura Ildikó 1 Kunčar, Ondřej 1 Lammich, Peter 1 Matichuk, Daniel 1 Paskevich, Andrei 1 Pattinson, Dirk 1 Peltier, Nicolas 1 Smolka, Steffen Juilf 1 Snelting, Gregor 1 Steckermeier, Albert 1 Sternagel, Christian 1 Sultana, Nik 1 Thiemann, René 1 Tinelli, Cesare all top 5 Serials 16 Journal of Automated Reasoning 3 Lecture Notes in Computer Science 2 Logical Methods in Computer Science 1 ACM Transactions on Computational Logic 1 Journal of Applied Logic 1 Journal of Formalized Reasoning Fields 59 Computer science (68-XX) 22 Mathematical logic and foundations (03-XX) 5 General and overarching topics; collections (00-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 51 Publications have been cited 481 times in 239 Documents Cited by ▼ Year ▼ Nitpick: a counterexample generator for higher-order logic based on a relational model finder. Zbl 1291.68326Blanchette, Jasmin Christian; Nipkow, Tobias 51 2010 Extending Sledgehammer with SMT solvers. Zbl 1314.68272Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. 36 2013 Truly modular (co)datatypes for Isabelle/HOL. Zbl 1416.68151Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy 27 2014 Extending Sledgehammer with SMT solvers. Zbl 1314.68271Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. 23 2011 Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias 22 2011 Hammering towards QED. Zbl 1451.68318Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef 22 2016 TFF1: the TPTP typed first-order form with rank-1 polymorphism. Zbl 1381.68260Blanchette, Jasmin Christian; Paskevich, Andrei 16 2013 Encoding monomorphic and polymorphic types. Zbl 1381.68259Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas 15 2013 MaSh: machine learning for Sledgehammer. Zbl 1317.68215Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef 14 2013 A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef 13 2016 Superposition with lambdas. Zbl 1471.03014Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe 13 2019 Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. Zbl 1362.68251Traytel, Dmitry; Popescu, Andrei; Blanchette, Jasmin C. 13 2012 Superposition for \(\lambda\)-free higher-order logic. Zbl 06958090Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe 12 2018 Semi-intelligible Isar proofs from machine-generated proofs. Zbl 1356.68178Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert 11 2016 Foundational extensible corecursion: a proof assistant perspective. Zbl 1360.68358Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 11 2015 Unified classical logic completeness. A coinductive pearl. Zbl 1409.68250Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 10 2014 Friends with benefits. Implementing corecursion in foundational proof assistants. Zbl 1485.68280Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy 10 2017 Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68306Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe 10 2018 A transfinite Knuth-Bendix order for lambda-free higher-order terms. Zbl 1496.03037Becker, Heiko; Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel 9 2017 Mining the Archive of Formal Proofs. Zbl 1417.68176Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias 8 2015 Soundness and completeness proofs by coinductive methods. Zbl 1409.68251Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 8 2017 More SPASS with Isabelle. Superposition with hard sorts and configurable simplification. Zbl 1360.68742Blanchette, Jasmin Christian; Popescu, Andrei; Wand, Daniel; Weidenbach, Christoph 8 2012 LEO-II and Satallax on the Sledgehammer test bench. Zbl 1262.68161Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C. 8 2013 A comprehensive framework for saturation theorem proving. Zbl 07614520Waldmann, Uwe; Tourret, Sophie; Robillard, Simon; Blanchette, Jasmin 8 2020 Superposition for full higher-order logic. Zbl 1497.03030Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar 8 2021 Cardinals in Isabelle/HOL. Zbl 1416.68152Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 6 2014 Mechanizing the metatheory of Sledgehammer. Zbl 1398.68479Blanchette, Jasmin Christian; Popescu, Andrei 6 2013 Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 1495.68238Biendarra, 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 Making higher-order superposition work. Zbl 07437092Vukmirović, Petar; Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Nummelin, Visa; Tourret, Sophie 6 2021 Encoding monomorphic and polymorphic types. Zbl 1445.68327Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas 6 2016 Scalable fine-grained proofs for formula processing. Zbl 1468.68278Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal 5 2020 Superposition for lambda-free higher-order logic. Zbl 07350767Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe 5 2021 A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1448.68457Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph 5 2018 A lambda-free higher-order recursive path order. Zbl 1486.68085Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel 5 2017 Superposition with lambdas. Zbl 07433023Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe 5 2021 Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68307Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe 4 2020 A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1475.68432Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph 4 2016 Model finding for recursive functions in SMT. Zbl 1475.68448Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare 4 2016 A decision procedure for (co)datatypes in SMT solvers. Zbl 1410.68337Reynolds, Andrew; Blanchette, Jasmin Christian 4 2017 A unifying splitting framework. Zbl 07437088Ebner, Gabriel; Blanchette, Jasmin; Tourret, Sophie 4 2021 A decision procedure for (co)datatypes in SMT solvers. Zbl 1465.68297Reynolds, Andrew; Blanchette, Jasmin Christian 3 2015 Witnessing (co)datatypes. Zbl 1335.68224Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 3 2015 Superposition with datatypes and codatatypes. Zbl 06958111Blanchette, Jasmin Christian; Peltier, Nicolas; Robillard, Simon 3 2018 Monotonicity inference for higher-order formulas. Zbl 1291.03016Blanchette, Jasmin Christian; Krauss, Alexander 3 2010 Monotonicity inference for higher-order formulas. Zbl 1266.03021Blanchette, Jasmin Christian; Krauss, Alexander 2 2011 Foundational nonuniform (co)datatypes for higher-order logic. Zbl 1457.68173Blanchette, Jasmin Christian; Meier, Fabian; Popescu, Andrei; Traytel, Dmitriy 1 2017 Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Zbl 1343.68004 1 2016 Scalable fine-grained proofs for formula processing. Zbl 1494.68280Barbosa, 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 A formal proof of the expressiveness of deep learning. Zbl 1468.68280Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich 1 2017 Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. Zbl 1434.03025Blanchette, Jasmin Christian; Fleury, Mathias; Traytel, Dmitriy 1 2017 Superposition for full higher-order logic. Zbl 1497.03030Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar 8 2021 Making higher-order superposition work. Zbl 07437092Vukmirović, Petar; Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Nummelin, Visa; Tourret, Sophie 6 2021 Superposition for lambda-free higher-order logic. Zbl 07350767Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe 5 2021 Superposition with lambdas. Zbl 07433023Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe 5 2021 A unifying splitting framework. Zbl 07437088Ebner, Gabriel; Blanchette, Jasmin; Tourret, Sophie 4 2021 A comprehensive framework for saturation theorem proving. Zbl 07614520Waldmann, Uwe; Tourret, Sophie; Robillard, Simon; Blanchette, Jasmin 8 2020 Scalable fine-grained proofs for formula processing. Zbl 1468.68278Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal 5 2020 Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68307Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe 4 2020 Superposition with lambdas. Zbl 1471.03014Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe 13 2019 Superposition for \(\lambda\)-free higher-order logic. Zbl 06958090Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe 12 2018 Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68306Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe 10 2018 A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1448.68457Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph 5 2018 Superposition with datatypes and codatatypes. Zbl 06958111Blanchette, Jasmin Christian; Peltier, Nicolas; Robillard, Simon 3 2018 Friends with benefits. Implementing corecursion in foundational proof assistants. Zbl 1485.68280Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy 10 2017 A transfinite Knuth-Bendix order for lambda-free higher-order terms. Zbl 1496.03037Becker, Heiko; Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel 9 2017 Soundness and completeness proofs by coinductive methods. Zbl 1409.68251Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 8 2017 Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 1495.68238Biendarra, 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.68085Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel 5 2017 A decision procedure for (co)datatypes in SMT solvers. Zbl 1410.68337Reynolds, Andrew; Blanchette, Jasmin Christian 4 2017 Foundational nonuniform (co)datatypes for higher-order logic. Zbl 1457.68173Blanchette, Jasmin Christian; Meier, Fabian; Popescu, Andrei; Traytel, Dmitriy 1 2017 Scalable fine-grained proofs for formula processing. Zbl 1494.68280Barbosa, Haniel; Blanchette, Jasmin Christian; Fontaine, Pascal 1 2017 A formal proof of the expressiveness of deep learning. Zbl 1468.68280Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich 1 2017 Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. Zbl 1434.03025Blanchette, Jasmin Christian; Fleury, Mathias; Traytel, Dmitriy 1 2017 Hammering towards QED. Zbl 1451.68318Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef 22 2016 A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef 13 2016 Semi-intelligible Isar proofs from machine-generated proofs. Zbl 1356.68178Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert 11 2016 Encoding monomorphic and polymorphic types. Zbl 1445.68327Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas 6 2016 A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1475.68432Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph 4 2016 Model finding for recursive functions in SMT. Zbl 1475.68448Reynolds, 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 1 2016 Foundational extensible corecursion: a proof assistant perspective. Zbl 1360.68358Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 11 2015 Mining the Archive of Formal Proofs. Zbl 1417.68176Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias 8 2015 A decision procedure for (co)datatypes in SMT solvers. Zbl 1465.68297Reynolds, Andrew; Blanchette, Jasmin Christian 3 2015 Witnessing (co)datatypes. Zbl 1335.68224Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 3 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.68151Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy 27 2014 Unified classical logic completeness. A coinductive pearl. Zbl 1409.68250Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 10 2014 Cardinals in Isabelle/HOL. Zbl 1416.68152Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 6 2014 Extending Sledgehammer with SMT solvers. Zbl 1314.68272Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. 36 2013 TFF1: the TPTP typed first-order form with rank-1 polymorphism. Zbl 1381.68260Blanchette, Jasmin Christian; Paskevich, Andrei 16 2013 Encoding monomorphic and polymorphic types. Zbl 1381.68259Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas 15 2013 MaSh: machine learning for Sledgehammer. Zbl 1317.68215Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef 14 2013 LEO-II and Satallax on the Sledgehammer test bench. Zbl 1262.68161Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C. 8 2013 Mechanizing the metatheory of Sledgehammer. Zbl 1398.68479Blanchette, Jasmin Christian; Popescu, Andrei 6 2013 Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. Zbl 1362.68251Traytel, Dmitry; Popescu, Andrei; Blanchette, Jasmin C. 13 2012 More SPASS with Isabelle. Superposition with hard sorts and configurable simplification. Zbl 1360.68742Blanchette, Jasmin Christian; Popescu, Andrei; Wand, Daniel; Weidenbach, Christoph 8 2012 Extending Sledgehammer with SMT solvers. Zbl 1314.68271Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. 23 2011 Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias 22 2011 Monotonicity inference for higher-order formulas. Zbl 1266.03021Blanchette, Jasmin Christian; Krauss, Alexander 2 2011 Nitpick: a counterexample generator for higher-order logic based on a relational model finder. Zbl 1291.68326Blanchette, Jasmin Christian; Nipkow, Tobias 51 2010 Monotonicity inference for higher-order formulas. Zbl 1291.03016Blanchette, Jasmin Christian; Krauss, Alexander 3 2010 all cited Publications top 5 cited Publications all top 5 Cited by 307 Authors 31 Blanchette, Jasmin Christian 19 Urban, Josef 18 Kaliszyk, Cezary 17 Benzmüller, Christoph Ewald 11 Guttmann, Walter 11 Popescu, Andrei 10 Reynolds, Andrew 10 Tourret, Sophie 9 Bentkamp, Alexander 9 Lochbihler, Andreas 9 Vukmirović, Petar 8 Barrett, Clark W. 8 Paulson, Lawrence Charles 8 Traytel, Dmitry 7 Foster, Simon 7 Tinelli, Cesare 7 Waldmann, Uwe 6 Fleury, Mathias 6 Jakubův, Jan 6 Sutcliffe, Geoff 5 Cruanes, Simon 5 Lammich, Peter 5 Reger, Giles 5 Weidenbach, Christoph 5 Zohar, Yoni 4 Abel, Andreas M. 4 Bhayat, Ahmed 4 Böhme, Sascha 4 Brown, Chad Edward 4 Fuenmayor, David 4 Kunčar, Ondřej 4 Niemetz, Aina 4 Nipkow, Tobias 4 Nummelin, Visa 4 Preiner, Mathias 4 Schlichtkrull, Anders 4 Steen, Alexander 4 Struth, Georg 4 Suda, Martin 4 Woodcock, James C. P. 3 Avigad, Jeremy 3 Barbosa, Haniel 3 Bonacina, Maria Paola 3 Chvalovský, Karel 3 Divasón, Jose 3 Färber, Michael 3 Fontaine, Pascal 3 From, Asta Halkjær 3 Gauthier, Thibault 3 Grabowski, Adam 3 Heule, Marijn J. H. 3 Janičić, Predrag 3 Koutsoukou-Argyraki, Angeliki 3 Momigliano, Alberto 3 Narboux, Julien 3 Norrish, Michael 3 Pąk, Karol 3 Rabe, Florian 3 Scott, Dana Stewart 3 Smallbone, Nicholas 3 Villadsen, Jørgen 3 Weber, Tjark 3 Yamada, Akihisa 3 Zeyda, Frank 2 Armstrong, Alasdair 2 Baek, Seulkee 2 Baumgartner, Peter 2 Berghammer, Rudolf 2 Brunner, Julian 2 Bundy, Alan 2 Cavalcanti, Ana 2 Claessen, Koen 2 Czajka, Łukasz 2 Desharnais, Martin 2 Duarte, André 2 Dubois, Catherine 2 Dubut, Jérémy 2 Fürer, Basil 2 Giorgetti, Alain 2 Grov, Gudmund 2 Guan, Yong 2 Halmagrand, Pierre 2 Heskes, Tom M. 2 Höfner, Peter 2 Hupel, Lars 2 Korovin, Konstantin 2 Krauss, Alexander 2 Kühlwein, Daniel 2 Lange, Jane 2 Lewis, Robert Y. 2 Li, Yongdong 2 Libal, Tomer 2 Olšák, Miroslav 2 Pease, Alison 2 Pientka, Brigitte 2 Pous, Damien 2 Raggi, Daniel 2 Ringeissen, Christophe 2 Robillard, Simon 2 Schneider, Joshua P. ...and 207 more Authors all top 5 Cited in 26 Serials 59 Journal of Automated Reasoning 8 Journal of Logical and Algebraic Methods in Programming 7 Logical Methods in Computer Science 5 Formal Aspects of Computing 5 AI Communications 3 Theoretical Computer Science 3 Journal of Functional Programming 2 Journal of Symbolic Computation 2 Experimental Mathematics 2 Annals of Mathematics and Artificial Intelligence 2 Theory and Practice of Logic Programming 2 ACM Transactions on Computational Logic 2 Mathematics in Computer Science 2 Logica Universalis 1 Acta Informatica 1 Artificial Intelligence 1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV) 1 Bulletin of the Section of Logic 1 Journal of Cryptology 1 MSCS. Mathematical Structures in Computer Science 1 Formal Methods in System Design 1 Journal of Logic, Language and Information 1 Advances in Applied Clifford Algebras 1 Fundamenta Informaticae 1 The Journal of Logic and Algebraic Programming 1 The Review of Symbolic Logic all top 5 Cited in 21 Fields 227 Computer science (68-XX) 82 Mathematical logic and foundations (03-XX) 5 Combinatorics (05-XX) 3 Information and communication theory, circuits (94-XX) 2 Linear and multilinear algebra; matrix theory (15-XX) 2 Category theory; homological algebra (18-XX) 2 Numerical analysis (65-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 General and overarching topics; collections (00-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 General algebraic systems (08-XX) 1 Number theory (11-XX) 1 Field theory and polynomials (12-XX) 1 Commutative algebra (13-XX) 1 Real functions (26-XX) 1 Probability theory and stochastic processes (60-XX) 1 Mechanics of particles and systems (70-XX) 1 Optics, electromagnetic theory (78-XX) 1 Operations research, mathematical programming (90-XX) 1 Systems theory; control (93-XX) 1 Mathematics education (97-XX) Citations by Year