default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJasmin Blanchette
Jasmin Christian Blanchette
Person information
- affiliation: Ludwig Maximilian University of Munich, Germany
- affiliation: Max Planck Institute for Informatics, Saarbrücken, Germany
- affiliation: University of Lorraine, Nancy, France
- affiliation (former): Vrije Universiteit Amsterdam, The Netherlands
- affiliation (former): Technical University of Munich, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[c64]Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret:
A Modular Formalization of Superposition in Isabelle/HOL. ITP 2024: 12:1-12:20- 2023
- [j43]Jasmin Christian Blanchette, Qi Qiu, Sophie Tourret:
Given Clause Loops. Arch. Formal Proofs 2023 (2023) - [j42]Alexander Bentkamp, Jasmin Blanchette
, Visa Nummelin, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann:
Mechanical Mathematicians. Commun. ACM 66(4): 80-90 (2023) - [j41]Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic:
Superposition for Higher-Order Logic. J. Autom. Reason. 67(1): 10 (2023) - [j40]Gabriel Ebner, Jasmin Blanchette, Sophie Tourret:
Unifying Splitting. J. Autom. Reason. 67(2): 16 (2023) - [j39]Jasmin Blanchette, Petar Vukmirovic:
SAT-Inspired Higher-Order Eliminations. Log. Methods Comput. Sci. 19(2) (2023) - [j38]Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Uwe Waldmann:
Complete and Efficient Higher-Order Reasoning via Lambda-Superposition. ACM SIGLOG News 10(4): 25-40 (2023) - [j37]Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule:
SAT-Inspired Eliminations for Superposition. ACM Trans. Comput. Log. 24(1): 7:1-7:25 (2023) - [c63]Jasmin Blanchette, Qi Qiu, Sophie Tourret:
Verified Given Clause Procedures. CADE 2023: 61-77 - [c62]Visa Nummelin, Jasmin Blanchette, Sander R. Dahmen:
Recurrence-Driven Summations in Automated Deduction. FroCoS 2023: 23-40 - [c61]Martin Dvorak, Jasmin Blanchette:
Closure Properties of General Grammars - Formally Verified. ITP 2023: 15:1-15:16 - [c60]Petar Vukmirovic, Jasmin Blanchette, Stephan Schulz:
Extending a High-Performance Prover to Higher-Order Logic. TACAS (2) 2023: 111-129 - [e7]Jasmin Blanchette, James H. Davenport, Peter Koepke, Michael Kohlhase, Andrea Kohlhase, Adam Naumowicz, Dennis Müller, Yasmine Sharoda, Claudio Sacerdoti Coen:
Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26 - 31, 2021. CEUR Workshop Proceedings 3377, CEUR-WS.org 2023 [contents] - [i7]Martin Dvorak, Jasmin Blanchette:
Closure Properties of Unrestricted Grammars - Formally Verified. CoRR abs/2302.06420 (2023) - 2022
- [j36]Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette:
A Comprehensive Framework for Saturation Theorem Proving. J. Autom. Reason. 66(4): 499-539 (2022) - [j35]Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret:
Making Higher-Order Superposition Work. J. Autom. Reason. 66(4): 541-564 (2022) - [j34]Petar Vukmirovic, Jasmin Blanchette, Simon Cruanes, Stephan Schulz:
Extending a brainiac prover to lambda-free higher-order logic. Int. J. Softw. Tools Technol. Transf. 24(1): 67-87 (2022) - [c59]Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel:
Seventeen Provers Under the Hammer. ITP 2022: 8:1-8:18 - [e6]Jasmin Blanchette, Laura Kovács, Dirk Pattinson:
Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings. Lecture Notes in Computer Science 13385, Springer 2022, ISBN 978-3-031-10768-9 [contents] - [i6]Jasmin Blanchette, Petar Vukmirovic:
SAT-Inspired Higher-Order Eliminations. CoRR abs/2208.07775 (2022) - 2021
- [j33]Jasmin Blanchette:
Message from the New Editor-in-Chief. J. Autom. Reason. 65(2): 155 (2021) - [j32]Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann:
Superposition with Lambdas. J. Autom. Reason. 65(7): 893-940 (2021) - [j31]Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann:
Superposition for Lambda-Free Higher-Order Logic. Log. Methods Comput. Sci. 17(2) (2021) - [c58]Gabriel Ebner, Jasmin Blanchette, Sophie Tourret:
A Unifying Splitting Framework. CADE 2021: 344-360 - [c57]Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic:
Superposition for Full Higher-order Logic. CADE 2021: 396-412 - [c56]Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret:
Making Higher-Order Superposition Work. CADE 2021: 415-432 - [c55]Sophie Tourret, Jasmin Blanchette:
A modular Isabelle framework for verifying saturation provers. CPP 2021: 224-237 - [c54]Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule:
SAT-Inspired Eliminations for Superposition. FMCAD 2021: 231-240 - [c53]Jasmin Blanchette, Adam Naumowicz:
FMM Preface. CICM Workshops 2021 - [i5]Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann:
Superposition with Lambdas. CoRR abs/2102.00453 (2021) - 2020
- [j30]Jasmin Blanchette, Sophie Tourret:
Extensions to the Comprehensive Framework for Saturation Theorem Proving. Arch. Formal Proofs 2020 (2020) - [j29]Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine:
Scalable Fine-Grained Proofs for Formula Processing. J. Autom. Reason. 64(3): 485-510 (2020) - [j28]Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann:
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. J. Autom. Reason. 64(7): 1169-1195 (2020) - [c52]Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette:
A Comprehensive Framework for Saturation Theorem Proving. IJCAR (1) 2020: 316-334 - [e5]Jasmin Blanchette, Catalin Hritcu:
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. ACM 2020, ISBN 978-1-4503-7097-4 [contents] - [i4]Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann:
Superposition for Lambda-Free Higher-Order Logic. CoRR abs/2005.02094 (2020)
2010 – 2019
- 2019
- [j27]Jasmin Christian Blanchette, Stephan Merz:
Selected Extended Papers of ITP 2016: Preface. J. Autom. Reason. 62(2): 169-170 (2019) - [j26]Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow:
A Formal Proof of the Expressiveness of Deep Learning. J. Autom. Reason. 63(2): 347-368 (2019) - [j25]Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel:
Bindings as bounded natural functors. Proc. ACM Program. Lang. 3(POPL): 22:1-22:34 (2019) - [j24]Jasmin Blanchette, Francis Bordeleau, Alfonso Pierantonio, Nikolai Kosmatov, Gabriele Taentzer, Manuel Wimmer:
Introduction to the STAF 2015 special section. Softw. Syst. Model. 18(1): 191-193 (2019) - [c51]Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann:
Superposition with Lambdas. CADE 2019: 55-73 - [c50]Jasmin Christian Blanchette:
Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). CPP 2019: 1-13 - [c49]Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel:
A verified prover based on ordered resolution. CPP 2019: 152-165 - [c48]Petar Vukmirovic, Jasmin Christian Blanchette, Simon Cruanes, Stephan Schulz:
Extending a Brainiac Prover to Lambda-Free Higher-Order Logic. TACAS (1) 2019: 192-210 - 2018
- [j23]Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann:
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs 2018 (2018) - [j22]Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel:
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs 2018 (2018) - [j21]Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting:
Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. 61(1-4): 1-8 (2018) - [j20]Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach:
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. Autom. Reason. 61(1-4): 333-365 (2018) - [c47]Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann:
Superposition for Lambda-Free Higher-Order Logic. IJCAR 2018: 28-46 - [c46]Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann:
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. IJCAR 2018: 89-107 - [c45]Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard:
Superposition with Datatypes and Codatatypes. IJCAR 2018: 370-387 - [c44]Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich:
A verified SAT solver with watched literals using imperative HOL. CPP 2018: 158-171 - 2017
- [j19]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Abstract Soundness. Arch. Formal Proofs 2017 (2017) - [j18]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Operations on Bounded Natural Functors. Arch. Formal Proofs 2017 (2017) - [j17]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Soundness and Completeness Proofs by Coinductive Methods. J. Autom. Reason. 58(1): 149-179 (2017) - [j16]Andrew Reynolds, Jasmin Christian Blanchette:
A Decision Procedure for (Co)datatypes in SMT Solvers. J. Autom. Reason. 58(3): 341-362 (2017) - [c43]Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann:
Towards Strong Higher-Order Automation for Fast Interactive Verification. ARCADE@CADE 2017: 16-23 - [c42]Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine:
Scalable Fine-Grained Proofs for Formula Processing. CADE 2017: 398-412 - [c41]Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand:
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. CADE 2017: 432-453 - [c40]Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel:
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. ESOP 2017: 111-140 - [c39]Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand:
A Lambda-Free Higher-Order Recursive Path Order. FoSSaCS 2017: 461-479 - [c38]Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel:
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS 2017: 3-21 - [c37]Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach:
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAI 2017: 4786-4790 - [c36]Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow:
A Formal Proof of the Expressiveness of Deep Learning. ITP 2017: 46-64 - [c35]Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel:
Foundational nonuniform (Co)datatypes for higher-order logic. LICS 2017: 1-12 - [c34]Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel:
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. FSCD 2017: 11:1-11:18 - [c33]Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine:
Language and Proofs for Higher-Order SMT (Work in Progress). PxTP 2017: 15-22 - [i3]Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, Cesare Tinelli:
Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). Dagstuhl Reports 7(9): 26-46 (2017) - 2016
- [j15]Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand:
Formalization of Knuth-Bendix Orders for Lambda-Free Higher-Order Terms. Arch. Formal Proofs 2016 (2016) - [j14]Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel:
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals. Arch. Formal Proofs 2016 (2016) - [j13]Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand:
Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms. Arch. Formal Proofs 2016 (2016) - [j12]Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone:
Encoding Monomorphic and Polymorphic Types. Log. Methods Comput. Sci. 12(4) (2016) - [j11]Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier:
Semi-intelligible Isar Proofs from Machine-Generated Proofs. J. Autom. Reason. 56(2): 155-200 (2016) - [j10]Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban:
A Learning-Based Fact Selector for Isabelle/HOL. J. Autom. Reason. 57(3): 219-244 (2016) - [j9]Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban:
Hammering towards QED. J. Formaliz. Reason. 9(1): 101-148 (2016) - [c32]Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach:
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAR 2016: 25-44 - [c31]Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli:
Model Finding for Recursive Functions in SMT. IJCAR 2016: 133-151 - [c30]Andrew Reynolds, Jasmin Christian Blanchette:
A Decision Procedure for (Co)datatypes in SMT Solvers. IJCAI 2016: 4205-4209 - [c29]Simon Cruanes, Jasmin Christian Blanchette:
Extending Nunchaku to Dependent Type Theory. HaTT@IJCAR 2016: 3-12 - [e4]Jasmin Christian Blanchette, Stephan Merz:
Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Lecture Notes in Computer Science 9807, Springer 2016, ISBN 978-3-319-43143-7 [contents] - [e3]Jasmin Christian Blanchette, Cezary Kaliszyk:
Proceedings First International Workshop on Hammers for Type Theories, HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016. EPTCS 210, 2016 [contents] - 2015
- [c28]Andrew Reynolds, Jasmin Christian Blanchette:
A Decision Procedure for (Co)datatypes in SMT Solvers. CADE 2015: 197-213 - [c27]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Witnessing (Co)datatypes. ESOP 2015: 359-382 - [c26]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Foundational extensible corecursion: a proof assistant perspective. ICFP 2015: 192-204 - [c25]Jasmin Christian Blanchette, Max W. Haslbeck, Daniel Matichuk, Tobias Nipkow:
Mining the Archive of Formal Proofs. CICM 2015: 3-17 - [e2]Jasmin Christian Blanchette, Nikolai Kosmatov:
Tests and Proofs - 9th International Conference, TAP@STAF 2015, L'Aquila, Italy, July 22-24, 2015. Proceedings. Lecture Notes in Computer Science 9154, Springer 2015, ISBN 978-3-319-21214-2 [contents] - [i2]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Foundational Extensible Corecursion. CoRR abs/1501.05425 (2015) - [i1]Nikolaj S. Bjørner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, Christoph Weidenbach:
Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). Dagstuhl Reports 5(9): 18-37 (2015) - 2014
- [j8]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Abstract Completeness. Arch. Formal Proofs 2014 (2014) - [c24]Jasmin Christian Blanchette:
My Life with an Automatic Theorem Prover. Vampire Workshop 2014: 1-7 - [c23]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Unified Classical Logic Completeness - A Coinductive Pearl. IJCAR 2014: 46-60 - [c22]Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel:
Experience report: the next 1100 Haskell programmers. Haskell 2014: 25-30 - [c21]Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel:
Truly Modular (Co)datatypes for Isabelle/HOL. ITP 2014: 93-110 - [c20]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Cardinals in Isabelle/HOL. ITP 2014: 111-127 - 2013
- [j7]Jasmin Christian Blanchette, Andrei Popescu:
Sound and Complete Sort Encodings for First-Order Logic. Arch. Formal Proofs 2013 (2013) - [j6]Nik Sultana, Jasmin Christian Blanchette, Lawrence C. Paulson:
LEO-II and Satallax on the Sledgehammer test bench. J. Appl. Log. 11(1): 91-102 (2013) - [j5]Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson:
Extending Sledgehammer with SMT Solvers. J. Autom. Reason. 51(1): 109-128 (2013) - [j4]Jasmin Christian Blanchette:
Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions. Softw. Qual. J. 21(1): 101-126 (2013) - [c19]Jasmin Christian Blanchette:
Redirecting Proofs by Contradiction. PxTP@CADE 2013: 11-26 - [c18]Steffen Juilf Smolka, Jasmin Christian Blanchette:
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. PxTP@CADE 2013: 117-132 - [c17]Jasmin Christian Blanchette, Andrei Paskevich:
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. CADE 2013: 414-420 - [c16]Jasmin Christian Blanchette, Andrei Popescu:
Mechanizing the Metatheory of Sledgehammer. FroCos 2013: 245-260 - [c15]Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban:
MaSh: Machine Learning for Sledgehammer. ITP 2013: 35-50 - [c14]Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone:
Encoding Monomorphic and Polymorphic Types. TACAS 2013: 493-507 - [e1]Jasmin Christian Blanchette, Josef Urban:
Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013. EPiC Series in Computing 14, EasyChair 2013 [contents] - 2012
- [b3]Jasmin Christian Blanchette:
Automatic proofs and refutations for higher-order logic. Technical University Munich, 2012, pp. 1-173 - [c13]Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach:
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. ITP 2012: 345-360 - [c12]Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette:
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. LICS 2012: 596-605 - 2011
- [j3]Jasmin Christian Blanchette, Alexander Krauss:
Monotonicity Inference for Higher-Order Formulas. J. Autom. Reason. 47(4): 369-398 (2011) - [c11]Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson:
Extending Sledgehammer with SMT Solvers. CADE 2011: 116-130 - [c10]Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow:
Automatic Proof and Disproof in Isabelle/HOL. FroCoS 2011: 12-27 - [c9]Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, Susmit Sarkar:
Nitpicking C++ concurrency. PPDP 2011: 113-124 - 2010
- [c8]Jasmin Christian Blanchette, Alexander Krauss:
Monotonicity Inference for Higher-Order Formulas. IJCAR 2010: 91-106 - [c7]Jasmin Christian Blanchette, Tobias Nipkow:
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. ITP 2010: 131-146 - [c6]Lawrence C. Paulson, Jasmin Christian Blanchette:
Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. IWIL@LPAR 2010: 1-11 - [c5]Jasmin Christian Blanchette:
Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod. LPAR short papers(Yogyakarta) 2010: 20-25 - [c4]Jasmin Christian Blanchette, Koen Claessen:
Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models. LPAR (Yogyakarta) 2010: 127-141 - [c3]