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