HOL(y) Hammer Learning-assisted automated reasoning for HOL Light

Request Advice:

Input the HOL Light formula to prove and select HOL Light session:

• HOL Light 193 Complex Analysis Emf193 Flyspeck Gödel's incompleteness theorem Infinite Ramsey's theorem Model of HOL Multivariate Analysis Ray193

Examples:

• Core HOL Light: &1 + &1 = &2 or ODD x \/ ODD (x + 1)
• Model: IS_RESULT r \/ IS_CLASH r
• Flyspeck: polyhedron p ==> convex (relative_interior p)

Upload Own Development:

Uploaded Developments

• HOL Light 193
• Complex Analysis
• Emf193
• Flyspeck
• Gödel's incompleteness theorem
• Infinite Ramsey's theorem
• Jordan Curve theorem
• Model of HOL
• Multivariate Analysis
• Ray193

Documentation:

• Cezary Kaliszyk and Josef Urban. Learning-assisted Automated Reasoning with Flyspeck. Arxiv.

Download (Local Install)

• Download source code: version 0.13.
• Unpack in your HOL Light directory and follow the instructions in the included README file.

Back to top