*To*: isabelle-users at cl.cam.ac.uk, Tobias Nipkow <nipkow at in.tum.de>, Christian Urban <christian.urban at kcl.ac.uk>*Subject*: Re: [isabelle] The HOL-Omega Tutorial is now available*From*: Peter Vincent Homeier <palantir at trustworthytools.com>*Date*: Mon, 4 Mar 2013 17:24:40 -0500*Cc*: Peter Vincent Homeier <palantir at trustworthytools.com>*In-reply-to*: <CAGneiuKJwKGsQt2scPvn0+Ju=msh0xq3X=UnhdWh4kUW9SWTrw@mail.gmail.com>*References*: <CAGneiuKJwKGsQt2scPvn0+Ju=msh0xq3X=UnhdWh4kUW9SWTrw@mail.gmail.com>*Sender*: phomeier at gmail.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 3:59 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)

- Previous by Date: [isabelle] ARiSVe 2013 final call for papers
- Next by Date: Re: [isabelle] Supporting native Unicode input in Isabelle/jEdit
- Previous by Thread: [isabelle] ARiSVe 2013 final call for papers
- Next by Thread: [isabelle] CfP CSASC "Proving in Math.Edu"
- Cl-isabelle-users March 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list