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 the HOL-Omega system may be found at
http://www.trustworthytools.com/id17.html
Sincerely,
Peter V. Homeier
--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
------------------------------------------------------------------------------
Free Next-Gen Firewall Hardware Offer
Buy your Sophos next-gen firewall before the end March 2013
and get the hardware for free! Learn more.
http://p.sf.net/sfu/sophos-d2d-feb
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
