Email Gateway (Aug 19 2022 at 10:03): Email Gateway (Aug 19 2022 at 10:03):From: Peter Vincent Homeier <palantir@trustworthytools.com>
I am pleased to announce that, as promised, the HOL-Omega Tutorial is now
available, at
http://www.trustworthytools.com/holw/tutorial.pdf
The HOL-Omega system is a significant extension of the popular and mature
HOL4 theorem prover, which has been under development for twenty-five
years. The HOL-Omega logic is virtually completely backwards compatible
with HOL4, so that libraries, applications, and developments written for
HOL4 will work in HOL-Omega without any changes, with very few exceptions.
HOL4 users are thus encouraged to investigate HOL-Omega without any loss of
functionality.
But HOL-Omega adds significant new power of interest to all users of
theorem provers, primarily centered around two key ideas, and what flows
from each:
(1) Types can be abstracted by type variables (similar to how terms are
abstracted by term variables in the lambda calculus).
--- Type operators are curried, so that they may take one argument at a
time.
--- Every type has a {\it kind}; kinds determine which type applications
are sensible.
--- Type variables can represent type operators.
(2) Terms can be abstracted by type variables (similar to System F).
--- The type of such an abstraction is a universal type.
--- Such an abstraction may be applied as a function to a type argument.
--- Such applications are managed by classifying all types into ranks.
These extensions of traditional higher order logic in a classical setting
were thought impossible for many years, proven to be inconsistent according
to Girard's paradox. But by the careful structuring of the type system by
ranks, soundness is maintained and Girard's paradox is defeated.
This means that unlike other advanced-logic theorem provers that restrain
their logics to an intuitionistic logic, HOL-Omega is a higher order logic
in a fully classical setting, where the law of the excluded middle holds,
equality of functions or predicates can be proven by extensionality, the
Hilbert epsilon operator is available for non-deterministic choice, and all
types are inhabited, supporting traditional HOL theorems like |- (!x. P x)
==> (?x. P x).
The effect of these design choices is that the HOL-Omega logic is much more
congenial, intuitive, and easy to work in than an intuitionistic logic,
while still providing the powerful new forms of abstraction listed above.
If the reader is interested and would like to try it, instructions for
obtaining and installing theHOL-Omega system may be found at
http://www.trustworthytools.com/id17.html
Sincerely,
Peter V. Homeier
Email Gateway (Aug 19 2022 at 10:38):From: Peter Vincent Homeier <palantir@trustworthytools.com>
There was a bug in the previous version of the HOL-Omega system which
prevented it from building with Poly/ML 5.5, the current version of Poly/ML.
This has been fixed and posted to the public repository for HOL-Omega, and
the current version should build correctly. If anyone has tried building HOL
-Omega and been frustrated, please try again with this new version of HOL-
Omega.
Many thanks to Robert Solovay for reporting this bug.
Sincerely,
Peter V. Homeier
Last updated: Nov 21 2024 at 12:39 UTC