Jasmin Christian Blanchette

Available identifiers

zbMath Open blanchette.jasmin-christianWikidataQ57515656 ScholiaQ57515656MaRDI QIDQ287335

List of research outcomes

Publication	Date of Publication	Type
https://portal.mardi4nfdi.de/entity/Q6123991	2024-04-08	Paper
SAT-Inspired Higher-Order Eliminations	2023-08-26	Paper
Unifying splitting	2023-06-27	Paper
Superposition for higher-order logic	2023-06-14	Paper
SAT-Inspired Eliminations for Superposition	2023-02-07	Paper
Making higher-order superposition work	2022-12-12	Paper
A comprehensive framework for saturation theorem proving	2022-12-12	Paper
A comprehensive framework for saturation theorem proving	2022-11-09	Paper
A unifying splitting framework	2021-12-01	Paper
Superposition for full higher-order logic	2021-12-01	Paper
Making higher-order superposition work	2021-12-01	Paper
Superposition with lambdas	2021-11-24	Paper
https://portal.mardi4nfdi.de/entity/Q4989394	2021-05-25	Paper
https://portal.mardi4nfdi.de/entity/Q5144617	2021-01-19	Paper
Formalizing Bachmair and Ganzinger's ordered resolution prover	2020-11-02	Paper
https://portal.mardi4nfdi.de/entity/Q5111307	2020-05-26	Paper
Superposition with lambdas	2020-03-10	Paper
Scalable fine-grained proofs for formula processing	2020-03-03	Paper
Hammering towards QED	2019-09-18	Paper
A formal proof of the expressiveness of deep learning	2019-08-21	Paper
Superposition for \(\lambda\)-free higher-order logic	2018-10-18	Paper
Superposition with datatypes and codatatypes	2018-10-18	Paper
Formalizing Bachmair and Ganzinger's ordered resolution prover	2018-10-18	Paper
A verified SAT solver framework with learn, forget, restart, and incrementality	2018-08-21	Paper
Foundational (co)datatypes and (co)recursion for higher-order logic	2018-01-04	Paper
A formal proof of the expressiveness of deep learning	2018-01-04	Paper
A transfinite Knuth-Bendix order for lambda-free higher-order terms	2017-09-22	Paper
Scalable fine-grained proofs for formula processing	2017-09-22	Paper
Soundness and completeness proofs by coinductive methods	2017-07-10	Paper
A decision procedure for (co)datatypes in SMT solvers	2017-06-29	Paper
A Lambda-Free Higher-Order Recursive Path Order	2017-05-19	Paper
Friends with Benefits	2017-05-19	Paper
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving	2017-05-16	Paper
Foundational extensible corecursion: a proof assistant perspective	2017-05-10	Paper
Encoding Monomorphic and Polymorphic Types	2017-04-11	Paper
A learning-based fact selector for Isabelle/HOL	2016-10-27	Paper
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality	2016-09-05	Paper
Model Finding for Recursive Functions in SMT	2016-09-05	Paper
Semi-intelligible Isar proofs from machine-generated proofs	2016-05-26	Paper
Witnessing (Co)datatypes	2016-04-26	Paper
A Decision Procedure for (Co)datatypes in SMT Solvers	2015-12-02	Paper
Mining the Archive of Formal Proofs	2015-11-20	Paper
Extending Sledgehammer with SMT solvers	2015-06-23	Paper
https://portal.mardi4nfdi.de/entity/Q4982446	2015-04-09	Paper
Unified Classical Logic Completeness	2014-09-26	Paper
Truly Modular (Co)datatypes for Isabelle/HOL	2014-09-08	Paper
Cardinals in Isabelle/HOL	2014-09-08	Paper
Mechanizing the Metatheory of Sledgehammer	2013-09-20	Paper
MaSh: Machine Learning for Sledgehammer	2013-08-07	Paper
Encoding Monomorphic and Polymorphic Types	2013-08-05	Paper
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism	2013-06-14	Paper
LEO-II and Satallax on the Sledgehammer test bench	2013-05-02	Paper
More SPASS with Isabelle	2012-09-20	Paper
Monotonicity inference for higher-order formulas	2012-07-31	Paper
Automatic Proof and Disproof in Isabelle/HOL	2011-10-07	Paper
Extending Sledgehammer with SMT Solvers	2011-07-29	Paper
Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models	2010-10-12	Paper
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder	2010-09-14	Paper
Monotonicity Inference for Higher-Order Formulas	2010-09-14	Paper
Proof pearl: Mechanizing the textbook proof of Huffman's algorithm	2009-09-01	Paper

Research outcomes over time

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Jasmin Christian Blanchette