Pages that link to "Item:Q2018657"
From MaRDI portal
The following pages link to HOL(y)Hammer: online ATP service for HOL Light (Q2018657):
Displaying 30 items.
- MizAR 40 for Mizar 40 (Q286800) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
- JEFL: joint embedding of formal proof libraries (Q831932) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Making PVS accessible to generic services by interpretation in a universal format (Q1687752) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
- Experiences from exporting major proof assistant libraries (Q2069875) (← links)
- Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
- A formally verified abstract account of Gödel's incompleteness theorems (Q2305432) (← links)
- Classification of alignments between concepts of formal mathematical systems (Q2364703) (← links)
- Automated Reasoning Service for HOL Light (Q2843009) (← links)
- Learning to Parse on Aligned Corpora (Rough Diamond) (Q2945635) (← links)
- Random Forests for Premise Selection (Q2964471) (← links)
- Higher-Order Modal Logics: Automation and Applications (Q2970308) (← links)
- Mining the Archive of Formal Proofs (Q3453102) (← links)
- Formalizing Physics: Automation, Presentation and Foundation Issues (Q3453125) (← links)
- System Description: E.T. 0.1 (Q3454109) (← links)
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description) (Q5049022) (← links)
- Matching Concepts across HOL Libraries (Q5495929) (← links)
- Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description (Q5495943) (← 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)
- (Q6079227) (← links)
- Machine Learning for Inductive Theorem Proving (Q6108816) (← links)
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction (Q6487292) (← links)
