Silver Falls

Welcome to the Gilith OpenTheory repo, which is currently storing 54 theory packages. Each theory package contains a collection of theorems together with their proofs. The proofs have been broken down into the primitive inferences of higher order logic, allowing them to be checked by computer.

This web interface is provided to help browse through the available packages, but the recommended way of downloading and processing theory packages is to use the opentheory package management tool. For more information on OpenTheory please refer to the project homepage.

Recently Uploaded Packages [more]

hol-base-1.2 — HOL basic theories
Uploaded 5 weeks ago by HOL OpenTheory Packager

m0-step-1.0 — M0 step evaluator
Uploaded 5 weeks ago by HOL OpenTheory Packager

m0-decomp-1.0 — M0 decompilation support
Uploaded 5 weeks ago by HOL OpenTheory Packager