The Coq mailing list

[Peter Vincent Homeier <palantir AT 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

On Sat, Feb 9, 2013 at 4:08 PM, Peter Vincent Homeier <palantir AT 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 theHOL-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)