The following pages link to Jasmin Christian Blanchette (Q287335):
Displaying 50 items.
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Monotonicity inference for higher-order formulas (Q438558) (← links)
- Proof pearl: Mechanizing the textbook proof of Huffman's algorithm (Q839031) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- Foundational (co)datatypes and (co)recursion for higher-order logic (Q1687535) (← links)
- Superposition for \(\lambda\)-free higher-order logic (Q1799065) (← links)
- Superposition with datatypes and codatatypes (Q1799098) (← links)
- LEO-II and Satallax on the Sledgehammer test bench (Q1948289) (← links)
- A unifying splitting framework (Q2055869) (← links)
- Superposition for full higher-order logic (Q2055874) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- A decision procedure for (co)datatypes in SMT solvers (Q2360873) (← links)
- Soundness and completeness proofs by coinductive methods (Q2362498) (← links)
- A transfinite Knuth-Bendix order for lambda-free higher-order terms (Q2405268) (← links)
- Witnessing (Co)datatypes (Q2802441) (← links)
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
- Model Finding for Recursive Functions in SMT (Q2817915) (← links)
- Mechanizing the Metatheory of Sledgehammer (Q2849493) (← links)
- Truly Modular (Co)datatypes for Isabelle/HOL (Q2879246) (← links)
- Cardinals in Isabelle/HOL (Q2879247) (← links)
- More SPASS with Isabelle (Q2914754) (← links)
- Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
- Foundational extensible corecursion: a proof assistant perspective (Q2981955) (← links)
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (Q2986838) (← links)
- A Lambda-Free Higher-Order Recursive Path Order (Q2988386) (← links)
- Friends with Benefits (Q2988636) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- Unified Classical Logic Completeness (Q3192180) (← links)
- Mining the Archive of Formal Proofs (Q3453102) (← links)
- A Decision Procedure for (Co)datatypes in SMT Solvers (Q3454092) (← links)
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism (Q4928456) (← links)
- Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models (Q4933301) (← links)
- (Q4982446) (← links)
- (Q4989394) (← links)
- (Q5111307) (← links)
- (Q5144617) (← links)
- Hammering towards QED (Q5195271) (← links)
- Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
- Encoding Monomorphic and Polymorphic Types (Q5326348) (← links)
- MaSh: Machine Learning for Sledgehammer (Q5327335) (← links)
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder (Q5747646) (← links)
- Monotonicity Inference for Higher-Order Formulas (Q5747753) (← links)
- SAT-Inspired Eliminations for Superposition (Q5875949) (← links)
- A formal proof of the expressiveness of deep learning (Q5915784) (← links)
- Formalizing Bachmair and Ganzinger's ordered resolution prover (Q5916290) (← links)
- Superposition with lambdas (Q5918381) (← links)
- Making higher-order superposition work (Q5918403) (← links)
- A comprehensive framework for saturation theorem proving (Q5918558) (← links)
- Making higher-order superposition work (Q5918575) (← links)
