HOLyHammer

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