Sledgehammer
From MaRDI portal
swMATH7047MaRDI QIDQ19106FDOQ19106
Author name not available (Why is that?)
Official website: http://isabelle.in.tum.de/website-Isabelle2009-1/sledgehammer.html
Cited In (only showing first 100 items - show all)
- A heuristic prover for real inequalities
- Mechanizing a process algebra for network protocols
- Semi-intelligible Isar proofs from machine-generated proofs
- A heuristic prover for real inequalities
- Mining the Archive of Formal Proofs
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- A formally verified proof of the central limit theorem
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- FALCON
- Automated and human proofs in general mathematics: an initial comparison
- Challenges and experiences in managing large-scale proofs
- BliStrTune
- IsaFoL
- DISCOUNT
- Lincx
- RADA
- Lifting
- Isabelle/UTP
- IDV
- ConCon
- FMLtoHOL
- Transfer
- DIAMOND
- GAPT
- SRASS
- WorkflowFM
- Celf
- Jordan
- kepler98
- conauto
- DPT
- embed_modal
- Abstract Completeness
- Algebraic Numbers
- Archive Formal Proofs
- Completeness theorem
- AVATAR
- FOL Fitting
- Knuth Bendix Orders
- Myhill-Nerode
- MadMax
- LLL Factorization
- Separation Logic
- Haskell Show Class
- Lambda Free RPOs
- DEMO
- AWN
- SAT Solver Verification
- Girth-Chromatic
- Imperative Refinement
- CoqHammer
- SMCDEL
- Stern-Brocot Tree
- Tame Graphs
- Stone Kleene
- Stone Algebras
- Twee
- DrACuLa
- VerifyThis
- Verified Prover
- ATOM
- Xml
- Robbins Conjecture
- DudeTM
- Mnemosyne
- LegalRuleML
- Worker/Wrapper Transformation
- Walnut
- Isabelle/DOF
- AxiomaticCategoryTheory
- AGES
- Certification_Monads
- Differential_Game_Logic
- FOL_Harrison
- GoedelGod
- Groebner_Bases
- GeoCoq
- Group-Ring-Module
- Kleene Algebra
- Matrix_Tensor
- Polynomials
- Relation Algebra
- Regular_Algebras
- SMTCoq
- Special_Function_Bounds
- Zipperposition
- Higher-order modal logics: automation and applications
- ATP and presentation service for Mizar formalizations
- SETL
- FlowFox
- PLM
- Zeta_3_Irrational
- Extending SMT solvers to higher-order logic
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- A decision procedure for (co)datatypes in SMT solvers
- A proof strategy language and proof script generation for Isabelle/HOL
- More SPASS with Isabelle
- Stone relation algebras
This page was built for software: Sledgehammer
