The following pages link to Sledgehammer (Q19106):
Displaying 50 items.
- Unifying Heterogeneous State-Spaces with Lenses (Q3179407) (← links)
- Mining the Archive of Formal Proofs (Q3453102) (← links)
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP (Q3453107) (← links)
- Automating Change of Representation for Proofs in Discrete Mathematics (Q3453117) (← links)
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners (Q3453128) (← links)
- A Decision Procedure for (Co)datatypes in SMT Solvers (Q3454092) (← links)
- Cooperating Proof Attempts (Q3454105) (← links)
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics (Q3455772) (← links)
- Contextual Natural Deduction (Q3455860) (← links)
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover (Q3460043) (← links)
- Closure, Properties and Closure Properties of Multirelations (Q3460617) (← links)
- Tool-Based Verification of a Relational Vertex Coloring Program (Q3460631) (← links)
- Computational logic: its origins and applications (Q4559535) (← links)
- αCheck: A mechanized metatheory model checker (Q4593089) (← links)
- Constraint solving for finite model finding in SMT solvers (Q4593094) (← links)
- Superposition for Bounded Domains (Q4913861) (← links)
- One Logic to Use Them All (Q4928425) (← links)
- PRocH: Proof Reconstruction for HOL Light (Q4928443) (← links)
- (Q4989394) (← links)
- (Q5028488) (← links)
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL (Q5049005) (← links)
- The CADE-28 Automated Theorem Proving System Competition – CASC-28 (Q5069650) (← links)
- A Hierarchy of Algebras for Boolean Subsets (Q5098719) (← links)
- Computer-Supported Exploration of a Categorical Axiomatization of Modeloids (Q5098730) (← links)
- Computer-Supported Analysis of Arguments in Climate Engineering (Q5098745) (← links)
- (Q5111307) (← links)
- Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument (Q5126209) (← links)
- The CADE-26 automated theorem proving system competition – CASC-26 (Q5145427) (← links)
- Programming and verifying a declarative first-order prover in Isabelle/HOL (Q5145439) (← links)
- Extracting verified decision procedures: DPLL and Resolution (Q5177337) (← links)
- Hammering towards QED (Q5195271) (← links)
- Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems (Q5200021) (← links)
- (Q5219924) (← links)
- (Q5219926) (← links)
- Stone Relation Algebras (Q5283207) (← links)
- Automating Theorem Proving with SMT (Q5327333) (← links)
- MaSh: Machine Learning for Sledgehammer (Q5327335) (← links)
- Extended Conscriptions Algebraically (Q5410482) (← links)
- Hipster: Integrating Theory Exploration in a Proof Assistant (Q5495917) (← links)
- Mining State-Based Models from Proof Corpora (Q5495930) (← links)
- Interactive Simplifier Tracing and Debugging in Isabelle (Q5495933) (← links)
- A Vernacular for Coherent Logic (Q5495937) (← links)
- Sledgehammer: Judgement Day (Q5747754) (← links)
- (Q5875442) (← links)
- A proof system for graph (non)-isomorphism verification (Q5883756) (← links)
- Superposition with lambdas (Q5918381) (← links)
- Making higher-order superposition work (Q5918403) (← links)
- Making higher-order superposition work (Q5918575) (← links)
- Superposition with lambdas (Q5919500) (← links)
- A formal proof of the expressiveness of deep learning (Q5919583) (← links)
