HOLyHammer
From MaRDI portal
Software:23493
swMATH11553MaRDI QIDQ23493FDOQ23493
Author name not available (Why is that?)
Cited In (30)
- Superposition with lambdas
- JEFL: joint embedding of formal proof libraries
- Formalizing Physics: Automation, Presentation and Foundation Issues
- Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description
- Aligning concepts across proof assistant libraries
- Mining the Archive of Formal Proofs
- A Modular Type Reconstruction Algorithm
- Making higher-order superposition work
- Superposition with lambdas
- Machine learning guidance for connection tableaux
- Classification of alignments between concepts of formal mathematical systems
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- A formally verified abstract account of Gödel's incompleteness theorems
- Random Forests for Premise Selection
- MizAR 40 for Mizar 40
- A learning-based fact selector for Isabelle/HOL
- Making higher-order superposition work
- Sharing HOL4 and HOL Light Proof Knowledge
- An abstraction-refinement framework for reasoning with large theories
- HOL(y)Hammer: online ATP service for HOL Light
- Learning-assisted theorem proving with millions of lemmas
- Experiences from exporting major proof assistant libraries
- Making PVS accessible to generic services by interpretation in a universal format
- Theorem proving as constraint solving with coherent logic
- Higher-Order Modal Logics: Automation and Applications
- Hammer for Coq: automation for dependent type theory
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- System Description: E.T. 0.1
- Hammering towards QED
- Matching Concepts across HOL Libraries
This page was built for software: HOLyHammer