HOLyHammer
From MaRDI portal
Cited in
(62)- MPTP
- gensim
- Aligning concepts across proof assistant libraries
- Hammer for Coq: automation for dependent type theory
- MoMM
- Making PVS accessible to generic services by interpretation in a universal format
- An abstraction-refinement framework for reasoning with large theories
- Sledgehammer
- MMT
- QMT
- Polar
- HOL(y)Hammer: online ATP service for HOL Light
- MaSh
- Machine learning guidance for connection tableaux
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- Experiences from exporting major proof assistant libraries
- Theorem proving as constraint solving with coherent logic
- PRocH
- Flyspeck
- A formally verified abstract account of Gödel's incompleteness theorems
- Classification of alignments between concepts of formal mathematical systems
- GQML
- AgsyHOL
- HOT
- Beagle
- SigmaKEE
- MizAR 40 for Mizar 40
- BliStr
- Random forests for premise selection
- Higher-order modal logics: automation and applications
- DISCOUNT
- LATIN
- LLFp
- A learning-based fact selector for Isabelle/HOL
- SRASS
- FMLtoHOL
- vis.js
- Mining the Archive of Formal Proofs
- Formalizing physics: automation, presentation and foundation issues
- System description: E.T. 0.1
- Sharing HOL4 and HOL Light proof knowledge
- VerifyThis
- Proofwatch
- Jinja not Java
- CoqHammer
- Holophrasm
- Zipperposition
- Whelp
- OpenTheory
- A Modular Type Reconstruction Algorithm
- Learning-assisted theorem proving with millions of lemmas
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- Hammering towards QED
- Matching concepts across HOL libraries
- Developing corpus-based translation methods between informal and formal mathematics: project description
- Superposition with lambdas
- Making higher-order superposition work
- Making higher-order superposition work
- Superposition with lambdas
- Robinson arithmetic
- EUCLID
- JEFL: joint embedding of formal proof libraries
This page was built for software: HOLyHammer
