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
On Sat, Feb 9, 2013 at 3:49 PM, Peter Vincent Homeier <
palan...@trustworthytools.com> wrote:
> 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)
--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
------------------------------------------------------------------------------
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_feb
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
