1 Aug 2012 07:00

## Re: rigorous axiomatic geometry proof in HOL Light

Sorry, Rob, I had a dumb typo, and meant to write "there exists a b such that a !~ b  (i.e. a ~ b is false)."

I'll ask you a question about my miz3 code, where the first few lines are

new_type("point",0);;
new_type_abbrev("point_set",:point->bool);;
new_constant("Between",:point->point->point->bool);;
new_constant("Line",:point_set->bool);;
new_constant("≡",:(point->bool)->(point->bool)->bool);;

I haven't read the manual carefully, but I see that you're working in something like a model of ZFC (except
there's no empty set), and that new_type' does not occur in the manual.  I see it occurs in the Description
I hope you can appreciate my confusion, as I'm working in HOL Light, and John Harrison's documentation
barely explains HOL, and he does not (I think) refer to your manuals.  A few dumb questions first:

Can we call your manual a HOL4 manual?  Do all version of HOL (e.g. HOL Light, Proof Power & Isabelle) abide by

My guess is that my new_type declaration of "point" says that there exists an un-named set of point, and that
any variable of type point will refer to an element of this set.  Is that right?  Let's call this set H, for
Hilbert plane.  The new_constant declaration of "Line" then says there's a predicate Line defined on the
power set P(H).   So later on when I write

let l be point_set;
let A B C be point;
assume Line l

I mean that the variable l refers to a subset of H, the variables A, B & C refer to elements of H, and that the


1 Aug 2012 08:08

### Re: rigorous axiomatic geometry proof in HOL Light

On Wed, Aug 1, 2012 at 6:00 AM, Bill Richter wrote:
new_type("point",0);;
new_type_abbrev("point_set",:point->bool);;
new_constant("Between",:point->point->point->bool);;
new_constant("Line",:point_set->bool);;
new_constant("≡",:(point->bool)->(point->bool)->bool);;

I haven't read the manual carefully, but I see that you're working in something like a model of ZFC (except there's no empty set), and that new_type' does not occur in the manual.  I see it occurs in the Description manual http://sourceforge.net/projects/hol/files/hol/kananaskis-7/kananaskis-7-description.pdf/download
I hope you can appreciate my confusion, as I'm working in HOL Light, and John Harrison's documentation barely explains HOL, and he does not (I think) refer to your manuals.  A few dumb questions first:

Can we call your manual a HOL4 manual?

Yes.

Do all version of HOL (e.g. HOL Light, Proof Power & Isabelle) abide by your Logic manual?

Roughly yes, with minor variations, except for Isabelle. Isabelle is a logical framework. Isabelle/HOL very roughly abides by the HOL4 Logic manual but the logic inherits some completely new features from the underlying framework.

It's the name of some lakes and a river in Alberta. (I think that's the intended reference.) It was adopted (as was "Athabasca"), as the name of a "generation" of HOL4 releases. We're up to Kananaskis release 7 (soon to be 8).

My guess is that my new_type declaration of "point" says that there exists an un-named set of point, and that any variable of type point will refer to an element of this set.  Is that right?  Let's call this set H, for Hilbert plane.  The new_constant declaration of "Line" then says there's a predicate Line defined on the power set P(H).   So later on when I write

let l be point_set;
let A B C be point;
assume Line l

I mean that the variable l refers to a subset of H, the variables A, B & C refer to elements of H, and that the subset l is actually a line, meaning that Line(l) = True.  Am I getting this right?  Can you explain an easy way I can cite this in my forthcoming geometry paper?

new_type and new_constant add new types and new constants to HOL by fiat. I suppose you must characterise them with new_axiom.
The HOL Logic Manual does not mention new_type because one of its aims is to build a model of HOL in set theory to give confidence that HOL is sound.
Once you use new_type or new_constant or new_axiom, the model described in the manual is no longer guaranteed to exist.
It's up to you to show that another model exists if you want people to believe your work isn't inconsistent.
(And it's hard to imagine doing so without first understanding the manual or something equivalent.)
But if you know roughly what your model would look like, and it fits within the existing HOL model (very likely), then there's no reason to declare new types and new constants by fiat and then prove that the resulting system is sound (outside of the proof assistant).
You can use HOL4's (and HOL Light's) mechanisms for definition! (You end up doing roughly the same proof, and you get the advantage of having it formalised and checked by the system.)
The manual does account for definitions of new types and constants by conservative extension and explicitly proves that such definitions are covered by the model in set theory that it develops.

BTW I recently adopted a better spin of my paper.  Before I was saying that I was improving Hartshorne's book Geometry: Euclid and Beyond, as a number of his proofs have gaps too wide for a high school student to leap.  Sounds kinda negativistic, right?  Now I say that I'm  continuing Hartshorne's great work by actually formalizing Hartshorne's Theorem 10.4, that all of Euclid's propositions in book I up to Prop (I.28) are true in any Hilbert plane, except for Props (I.1) and (I.22), which require extra axioms.

--
Best,
Bill

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

1 Aug 2012 09:29

### Re: rigorous axiomatic geometry proof in HOL Light

Ramana,

> new_type and new_constant add new types and new constants to HOL
> by fiat.

What these functions do is introduce new names into the available
vocabulary (or signatures and type signatures to use the terminologies of
the LOGIC manual). This is a conservative extension mechanism. For
new_constant, it is equivalent to a constant_specification with defining
property T. new_type has no equivalent in terms of type_specification,
because when it imposes no restriction on the cardinality of the new type,
so it really ought to be in the LOGIC manual.

> I
> suppose you must characterise them with new_axiom.

This is not true. IF all you need to know of a types is that it is
non-empty or of a constant that it has a given type, then you have no need
to use new_axiom in conjunction with new_type and new_constant. This is
precisely what Bill is doing, I believe.

It is not very common to work like this, because the theory you get is not
very suitable for reuse. It is more common to use type variables for
unknown types and variable parameters for unknown objects, so that they
can be instantiated to particular models. However, working with the
unspecified types and constants you get from new_type and new_constant is
a perfectly good approach and can be clearer if the theory you want is
just intended as a thing to be read and appreciated in its own right.

> The HOL Logic Manual does not mention new_type because one of its aims is
> to build a model of HOL in set theory to give confidence that HOL is
> sound.
> Once you use new_type or new_constant or new_axiom, the model described in
> the manual is no longer guaranteed to exist.

What you say about new_axiom is true. Once you use new_axiom, it is down
to you do produce some argument of your own as to the consistency of the
resulting system. What you say about new_type or new_constant is wrong,
see above.

Regards,

Rob.

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

1 Aug 2012 09:33

### Re: rigorous axiomatic geometry proof in HOL Light

Thank you Rob! I was hoping for someone to clear up my mistakes and teach me something more about conservative extension :)
(I may come off sounding confident but usually I am not.)
Also, Bill if you're not using new_axiom, then sorry for any offence caused by the tone of my previous email.

On Wed, Aug 1, 2012 at 8:29 AM, wrote:
Ramana,

> new_type and new_constant add new types and new constants to HOL
> by fiat.

What these functions do is introduce new names into the available
vocabulary (or signatures and type signatures to use the terminologies of
the LOGIC manual). This is a conservative extension mechanism. For
new_constant, it is equivalent to a constant_specification with defining
property T. new_type has no equivalent in terms of type_specification,
because when it imposes no restriction on the cardinality of the new type,
so it really ought to be in the LOGIC manual.

> I
> suppose you must characterise them with new_axiom.

This is not true. IF all you need to know of a types is that it is
non-empty or of a constant that it has a given type, then you have no need
to use new_axiom in conjunction with new_type and new_constant. This is
precisely what Bill is doing, I believe.

It is not very common to work like this, because the theory you get is not
very suitable for reuse. It is more common to use type variables for
unknown types and variable parameters for unknown objects, so that they
can be instantiated to particular models. However, working with the
unspecified types and constants you get from new_type and new_constant is
a perfectly good approach and can be clearer if the theory you want is
just intended as a thing to be read and appreciated in its own right.

> The HOL Logic Manual does not mention new_type because one of its aims is
> to build a model of HOL in set theory to give confidence that HOL is
> sound.
> Once you use new_type or new_constant or new_axiom, the model described in
> the manual is no longer guaranteed to exist.

What you say about new_axiom is true. Once you use new_axiom, it is down
to you do produce some argument of your own as to the consistency of the
resulting system. What you say about new_type or new_constant is wrong,
see above.

Regards,

Rob.

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

2 Aug 2012 09:03

### Re: rigorous axiomatic geometry proof in HOL Light

Thanks, Ramana and Rob!  As Rob says, I don't use new_axiom to define by type "point", but I do use new_axiom to
define Hilbert's geometry axioms, so I took no offense.  I would definitely prefer to use neither new_type
nor new_axiom. I'm using what John set me up with, but I think he thought of it as more of a way to get started,
rather than the best way to formalize Euclid's book 1.  BTW I don't think either of you answered my question

> the variable l refers to a subset of H, the variables A, B & C
> refer to elements of H, and that the subset l is actually a line,
> meaning that Line(l) =True.  Am I getting this right?

I would prefer to say that a Hilbert plane is a set H with two relations, Between and ===, with a predicate Line
defined on subsets of H, so that H satisfies the axioms I1--3, B1--4 and C1--6.  That's how I wrote my Tarski
geometry Mizar code.  I wasn't quite happy with that, and folks certainly believe that Hilbert's axioms
are consistent.  But I would like to know how to avoid new_type nor new_axiom.  It's possible that miz3 could
not handle the extra set theory load, as John suggested, and he said he'd improve the miz3 set theory
capacity when he returned.  Neither of you addressed

> John Harrison's documentation barely explains HOL, and he does
> not (I think) refer to your manuals.

Do you agree with me?  What is to be made of this?  I mean, if one uses new_type in HOL Light, what theorems is HOL
Light supposed to be formalizing?  I don't know where John writes anything stronger about types than on p 13
of his tutorial:

A key feature of HOL is that every term has a well-defined
type. Roughly speaking, the type indicates what kind of
mathematical object the term represents (a number, a set, a
function, etc.)

--

--
Best,
Bill

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

2 Aug 2012 09:25

### Re: rigorous axiomatic geometry proof in HOL Light

On Thu, Aug 2, 2012 at 8:03 AM, Bill Richter wrote:
Thanks, Ramana and Rob!  As Rob says, I don't use new_axiom to define by type "point", but I do use new_axiom to define Hilbert's geometry axioms, so I took no offense.  I would definitely prefer to use neither new_type nor new_axiom. I'm using what John set me up with, but I think he thought of it as more of a way to get started, rather than the best way to formalize Euclid's book 1.  BTW I don't think either of you answered my question

> the variable l refers to a subset of H, the variables A, B & C
> refer to elements of H, and that the subset l is actually a line,
> meaning that Line(l) =True.  Am I getting this right?

I would prefer to say that a Hilbert plane is a set H with two relations, Between and ===, with a predicate Line defined on subsets of H, so that H satisfies the axioms I1--3, B1--4 and C1--6.

Yes, you can certainly say that all with definitions.
Define a four-argument predicate

Hilbert_plane H (Between) (===) Line = axiom_1_holds /\ axiom_2_holds /\ ...

and use that as a hypothesis on all your theorems.
H, Between, ===, and Line, will all be variables that you universally quantify over, but restrict with the hypothesis Hilbert_plane.
Apart from avoiding new_axiom, this has the additional benefit of making your results reusable: anyone can provide whatever H, Between, ===, and Line they want by specialising one of your theorems and their obligation is to show that their combination satisfies all the axioms then they get your result as a conclusion.

That's how I wrote my Tarski geometry Mizar code.  I wasn't quite happy with that, and folks certainly believe that Hilbert's axioms are consistent.  But I would like to know how to avoid new_type nor new_axiom.

I described how above. And we have discussed this before. See for example http://sourceforge.net/mailarchive/message.php?msg_id=29172311

It's possible that miz3 could not handle the extra set theory load, as John suggested, and he said he'd improve the miz3 set theory capacity when he returned.  Neither of you addressed

> John Harrison's documentation barely explains HOL, and he does
> not (I think) refer to your manuals.

Do you agree with me?  What is to be made of this?
I mean, if one uses new_type in HOL Light, what theorems is HOL Light supposed to be formalizing?  I don't know where John writes anything stronger about types than on p 13 of his tutorial:

A key feature of HOL is that every term has a well-defined
type. Roughly speaking, the type indicates what kind of
mathematical object the term represents (a number, a set, a
function, etc.)

--
Best,
Bill

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

2 Aug 2012 23:48

### Re: rigorous axiomatic geometry proof in HOL Light

Thanks, Ramana!  I don't quite understand.  In each theorem I should
make an extra hypothesis which will look something like assume
Hilbert_plane H (Between) (===) Line {HP};
And I'll add the label HP to each "by" list in which I refer to one of
my earlier theorems?  In your earlier post, I think you said you
preferred shallow embeddings.  Do you call this a shallow embedding?

Back to my earlier question, my miz3 code begins
new_type("point",0);;
new_type_abbrev("point_set",:point->bool);;
new_constant("Line",:point_set->bool);;
I still don't know what the HOL, or HOL4 meaning of this is, but I have a new conjecture:
My new_type command defines a set called "point",  And later when I write
let A B C be point;
that means that the variables A, B & C refer to elements of the set "point"  Does that sound right?  In
particular, a type is the name of a set?

I'm having trouble with the term HOL.  If someone asked me to describe what HOL Light was doing, I'd say that we
were working in a model of ZFC with some extra features. E.g. it's quite difficult in ZFC to construct the
real line R (see Halmos's book Naive Set Theory), but HOL Light hands us a nice copy of R with all its
properties.  So if one did not have a model of ZFC, one would be doing FOL, just manipulating the f.o. ZFC
axioms, but it's a lot nice to actually have a model of ZFC, i.e. a collection of sets.  I don't mean that we
have all the sets that a model of ZFC would contain.  There's a set UNIV, the universe we work in, and a ZFC
model would not contain that.   All this is great, but I don't know why we're using the term HOL to describe it.
I understand that HOL means 2nd order
logic, 3rd order logic etc, but that just means you can quantify over more and more complicated sets, and I
guess we get all those sets in a model of ZFC.

I'm also confused about the HOL Logic manual saying we don't get the empty set.  I use the empty set all the
time, it's called EMPTY or [ {}, defined in sets.ml.  Maybe there's a technicality which going like this.  In
sets.ml, sets are "constructed" as boolean functions.  So (assuming that "point" is actually a set, as I
conjectured above) we can define the empty subset of point as the function
{}: point -> bool
which takes every element of point to False.  So is that it, we can get the empty set by confusing sets with
boolean functions?

--

--
Best,
Bill

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

3 Aug 2012 06:49

### Re: rigorous axiomatic geometry proof in HOL Light

On 03/08/12 07:48, Bill Richter wrote:
> Back to my earlier question, my miz3 code begins new_type("point",0);;
> new_type_abbrev("point_set",:point->bool);;
> new_constant("Line",:point_set->bool);; I still don't know what the HOL, or
> HOL4 meaning of this is, but I have a new conjecture: My new_type command
> defines a set called "point",  And later when I write let A B C be point;
> that means that the variables A, B & C refer to elements of the set "point"
> Does that sound right?  In particular, a type is the name of a set?

A non-polymorphic type denotes a non-empty ZFC set.  We can assume that this set
is one of the "non-empty sets in the von Neumann cumulative hierarchy formed
before stage ω + ω" (Logic Manual, p10)

A polymorphic type is a effectively a function on types; when you instantiate
the type variables you are applying the function to arguments and getting back
an actual non-empty set.

When you do a new_type command, the system picks an arbitrary non-empty set and
identifies your chosen name with that set.  Logically, you know nothing at all
about that type except that it is non-empty.

> I'm also confused about the HOL Logic manual saying we don't get the empty
> set.  I use the empty set all the time, it's called EMPTY or {}, defined in
> sets.ml.  Maybe there's a technicality which going like this.  In sets.ml,
> sets are "constructed" as boolean functions.  So (assuming that "point" is
> actually a set, as I conjectured above) we can define the empty subset of
> point as the function {}: point -> bool which takes every element of point to
> False.  So is that it, we can get the empty set by confusing sets with
> boolean functions?

Yes, the empty set, {}, that you are referring to is just a predicate (the
predicate that is everywhere false) over a type.  Alternatively, it is a subset
of a non-empty set.  If you read something saying that there is no empty set,
it's meaning that there is no empty type.

It is true that we can't do anything in HOL that you couldn't do in ZFC/FOL, but
things tend to work more smoothly in HOL.  In particular, there is no
distinction between predicates and 'sets', and no need for axioms restricting
what you can and can't write with a set comprehension.  This is because all such
predicates, sets and comprehensions are all done with respect to some bounding
set in the ZFC model.

HOL's handling of functions is also cleaner.  In FOL, you can't quantify over a
function-symbol, so it's illegal to write

∃f. ∀n. f (n + 1) < f (n)

where f is a function symbol of the FOL.  But, of course, mathematicians are
working in ZFC and sets can be held to represent functions, so you *are*
allowed to write

∃f ∈ N × N. ∀n ∈ N. f  (n + 1) < f  n

where the "function" f is really just a set, and the function symbols are
actually  ("function application"), + and × (in the outer quantification).

The meta-theory of FOL tells us that we can introduce fresh function symbols in
certain circumstances, so we might be able to create formulas that use f as a
function symbol, but that f can't be the same as the f which is just a subset of
N × N, even if it's behaviour looks pretty similar.  This is pretty yucky, and
HOL hides lots of complexity.

Michael

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

5 Aug 2012 11:42

### Re: rigorous axiomatic geometry proof in HOL Light


On 3 Aug 2012, at 05:49, Michael Norrish wrote:

> On 03/08/12 07:48, Bill Richter wrote:
>> Back to my earlier question, my miz3 code begins new_type("point",0);;
>> new_type_abbrev("point_set",:point->bool);;
>> new_constant("Line",:point_set->bool);; I still don't know what the HOL, or
>> HOL4 meaning of this is, but I have a new conjecture: My new_type command
>> defines a set called "point",  And later when I write let A B C be point;
>> that means that the variables A, B & C refer to elements of the set "point"
>> Does that sound right?  In particular, a type is the name of a set?
>
> A non-polymorphic type denotes a non-empty ZFC set.  We can assume that this set
> is one of the "non-empty sets in the von Neumann cumulative hierarchy formed
> before stage ω + ω" (Logic Manual, p10)

That isn't quite right. What the Logic Manual correctly says is that the set-theoretic universe in which
HOL types and terms take their values is closed under certain operations and that the set of sets you
mention (V_{\omega+\omega}) is a possible universe. It doesn't say that V_{\omega+\omega} is the
universe and the axioms don't imply any upper bound on the cardinality of types.
>
> A polymorphic type is a effectively a function on types; when you instantiate
> the type variables you are applying the function to arguments and getting back
> an actual non-empty set.
>
> When you do a new_type command, the system picks an arbitrary non-empty set and
> identifies your chosen name with that set.  Logically, you know nothing at all
> about that type except that it is non-empty.

Quite so. In particular, you don't know anything else about its cardinality. It could be
V_{\omega+\omega} itself or something much bigger. It would be consistent (but not conservative) to use
new_axiom to assert that a type introduced with new_type was a model of HOL or of ZFC, say. This is why I said
in a reply to Ramana the other day that new_type really should be accounted for in the Logic Manual:
new_constant is equivalent to a special case of constant specification but new_type is not equivalent to
a special case of type definition.

Regards,

Rob.

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

5 Aug 2012 14:13

### Re: rigorous axiomatic geometry proof in HOL Light

On 5/08/12 7:42 PM, Rob Arthan wrote:

>> A non-polymorphic type denotes a non-empty ZFC set.  We can assume
>> that this set is one of the "non-empty sets in the von Neumann
>> cumulative hierarchy formed before stage ω + ω" (Logic Manual,
>> p10)

> That isn't quite right. What the Logic Manual correctly says is that
> the set-theoretic universe in which HOL types and terms take their
> values is closed under certain operations and that the set of sets
> you mention (V_{\omega+\omega}) is a possible universe. It doesn't
> say that V_{\omega+\omega} is the universe and the axioms don't imply
> any upper bound on the cardinality of types.

Yes, I was sloppy there.

Michael


------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

3 Aug 2012 05:43

### Re: rigorous axiomatic geometry proof in HOL Light

   Define a four-argument predicate
Hilbert_plane H (Between) (===) Line = axiom_1_holds /\ axiom_2_holds /\
...
and use that as a hypothesis on all your theorems.

Thanks, Ramana!  The code below indicates that I can get rid of new_axiom following your suggestion.  I
should have seen this myself before, but I was bogged down in the set theory which I still don't know how to
pull off, so I didn't even try.  So thanks!

I kept the new_type stuff, and made TarskiModel a 0-argument predicate, and proved the first 4 theorems of
my Tarski axiomatic geometry http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml

EquivReflexive : thm = |- TarskiModel ==> (!a b. a,b === a,b)
EquivSymmetric : thm =
|- TarskiModel ==> (!a b c d. a,b === c,d ==> c,d === a,b)
EquivTransitive : thm =
|- TarskiModel
==> (!a b p q r s. a,b === p,q ==> p,q === r,s ==> a,b === r,s)
Baaa_THM : thm =
|- TarskiModel ==> (!a b. Between (a,a,a) /\ a,a === b,b)

I'm not too happy about the extra clutter caused by the statement TarskiModel, the label TM I use to refer to
it, and turning the axioms into theorems.  But that's great that I can get rid of new_axiom at least, so
thanks.

I don't know how to get rid of new_type using H and your 4-arg predicate.   I tried this, and I got the error
message
#     Exception: Failure "term after binary operator expected":

parse_as_infix("===",(12, "right"));;
let A1_DEF = new_definition
A1axiom  T  ===  <=>  !a b. T a /\ T b  ==>  a,b === b,a;;

I can appreciate this error message.  I want to say that T is a set and a belongs to T (or T a = True, or T a), but I
don't see how I can do that without some typing.  What do I even want the type of a, b & T to be here?

This seems to be a question of how to implement sets in HOL Light.

--
Best,
Bill

horizon := 0;;

new_type("point",0);;
new_constant("===",:point#point->point#point->bool);;
new_constant("Between",:point#point#point->bool);;

parse_as_infix("===",(12, "right"));;

let A1_DEF = new_definition
A1axiom  <=>  !a b. a,b === b,a;;

let A2_DEF = new_definition
A2axiom  <=>  !a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s;;

let A3_DEF = new_definition
A3axiom  <=>  !a b c. a,b === c,c ==> a = b;;

let A4_DEF = new_definition
A4axiom  <=>  !a q b c. ?x. Between(q,a,x) /\ a,x === b,c;;

let TarskiModel_DEF = new_definition
TarskiModel  <=>  A1axiom /\ A2axiom /\ A3axiom /\ A4axiom;;

let A1 = thm ;
TarskiModel  ==>  !a b. a,b === b,a
by TarskiModel_DEF, A1_DEF;;

let A2 = thm ;
TarskiModel  ==>  !a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s
by TarskiModel_DEF, A2_DEF;;

let A3 = thm ;
TarskiModel  ==>  !a b c. a,b === c,c ==> a = b
by TarskiModel_DEF, A3_DEF;;

let A4 = thm ;
TarskiModel  ==>  !a q b c. ?x. Between(q,a,x) /\ a,x === b,c
by TarskiModel_DEF, A4_DEF;;

let EquivReflexive = thm ;
TarskiModel  ==> !a b. a,b === a,b

proof
assume TarskiModel [TM];
let a b be point;
b,a === a,b by A1, TM;
qed by -, A2, TM;;

let EquivSymmetric = thm ;
assume TarskiModel [TM];
let a b c d be point;
assume a,b === c,d [1];
thus c,d === a,b

proof
a,b === a,b by EquivReflexive, TM;
qed by -, 1, A2, TM;;

let EquivTransitive = thm ;
assume TarskiModel [TM];
let a b p q r s be point;
assume a,b === p,q [H1];
assume p,q === r,s [H2];
thus a,b === r,s

proof
p,q === a,b by H1, EquivSymmetric, TM;
qed by -, H2, A2, TM;;

let Baaa_THM = thm ;
assume TarskiModel [TM];
let a b be point;
thus Between (a,a,a) /\ a,a === b,b

proof
consider x such that
Between (a,a,x) /\ a,x === b,b [X1] by A4, TM;
a = x by -, A3, TM;
qed by -, X1;;

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

3 Aug 2012 06:06

### Re: rigorous axiomatic geometry proof in HOL Light

On 03/08/12 13:43, Bill Richter wrote:
> I don't know how to get rid of new_type using H and your 4-arg predicate.   I
> tried this, and I got the error message #     Exception: Failure "term after
> binary operator expected":

> parse_as_infix("===",(12, "right"));; let A1_DEF = new_definition A1axiom  T
> ===  <=>  !a b. T a /\ T b  ==>  a,b === b,a;;

> I can appreciate this error message.  I want to say that T is a set and a
> belongs to T (or T a = True, or T a), but I don't see how I can do that
> without some typing.  What do I even want the type of a, b & T to be here?

> This seems to be a question of how to implement sets in HOL Light.

You could do it by replacing your concrete type point with a type variable.
See

type_of MAP

for syntax.  (In HOL4 and SML, you'd get (:'a->'b) -> 'a list -> 'b list, but I
have this feeling that HOL Light does things a little differently.)

But, first: the issue you have with your parameterised axioms and === is caused
by the fact that you need a way of "stripping" === of its special infix status.

So, I'd suggest:

A1axiom T (===) <=> !a b. T a /\ T b ==> a,b === b,a

Do this without pre-committing to any types at all and your definition will be
suitably polymorphic.

Ultimately, you'd have theorems of the form

TarskiModel T (===) ==> ...some conclusion...

From skimming your sources very superficially, it looks as if the Between
'constant' would need to be a parameter of TarskiModel too.

It also looks as if you could dispense with the T parameter, and just have

A1axiom (===) <=> !a b. a,b === b,a

Again, not defining any types in advance would give you something suitably
polymorphic.

As you noted, doing things this way is likely to be rather painful because you
will constantly have this annoying TarskiModel hypothesis hanging around.

Michael

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

5 Aug 2012 09:56

### Re: rigorous axiomatic geometry proof in HOL Light

   It also looks as if you could dispense with the T parameter, and just have

A1axiom (===) <=> !a b. a,b === b,a

Thanks, Michael, it works!!!  Whether or not I use first

parse_as_infix("===",(12, "right"));;

But I think that's only because === is already declared to be an infix.  I don't know why you parenthesized
===, but it seems to be needed.   I'll try to post working code soon.  Can you explain why this works, when a and b
don't have types?  Or what it even means?  To me, === is a 4-ary relation on set T.  On to your other points:

You could do it by replacing your concrete type point with a type variable.
See

type_of MAP

for syntax.  (In HOL4 and SML, you'd get (:'a->'b) -> 'a list -> 'b list, but I
have this feeling that HOL Light does things a little differently.)

Cool, I tried in HOL Light
type_of MAP;;
hol_type = :(?134838->?134839)->(?134838)list->(?134839)list

I think that's a cryptic version of what you said, because the HOL html reference manual say
map : ('a -> 'b) -> 'a list -> 'b list
map f [x1;...;xn] returns [(f x1);...;(f xn)].

That's the map function I'm used to from Scheme.  Strangely enough map has a different hol_type than MAP:
type_of map;;
val it : hol_type = :?134840

I guess that's what polymorphism means: map works for any types a and b.  I think I'm already using
polymorphism in my Hilbert code, e.g.:

let BiggerThanSingleton_THM = thm ;
let p be A->bool;
let x be A;
assume x IN p     [H1];
assume ~(p = {x})     [H2];
thus ? a . a IN p /\ ~(a = x)

proof
{x} SUBSET p     by H1, SING_SUBSET;
~(p SUBSET {x})     by -,  H2, SUBSET_ANTISYM;
consider a such that
a IN p /\ a NOTIN {x}     [X1] by -, SUBSET, NOTIN;
~(a = x)     by -, IN_SING, NOTIN;
qed     by -, X1;;

I don't know where I got the idea of using A as a type instead of 'a, or what 'a means, but to me, A stands for any
type, and it works in my Hilbert code, A apparently being replaced by point.

Here's another dumb question, for Freek maybe:  It's been obvious to me for some time that much of sets.ml
could be proved quite easily in miz3.   But that's awkward if we can't load in such a file with miz3 stuff in it.
Why doesn't use work for miz3 code, as in #use "hol.ml";; ?

--

--
Best,
Bill

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

5 Aug 2012 12:49

### Re: rigorous axiomatic geometry proof in HOL Light

Michael, your polymorphism worked!  Following your advice, I coded up in miz3, without new_type or
new_axiom, my first 7 Tarski axiomatic geometry theorems of http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml
I'm stuck on the next result because I don't know how to rewrite my definition

parse_as_infix("cong",(12, "right"));;

let cong_DEF = new_definition
a,b,c cong x,y,z <=>
a,b === x,y /\ a,c === x,z /\ b,c === y,z;;

My problem, I think, is that cong is now a function of ===, which is now a variable being passed around.  Here's
my miz3 code below, which I really enjoyed writing, as it took quite a bit of fiddling to get right.  Let me try
to explain why your polymorphism works on axiom A4, on which HOL-Light/miz3 prints out

val A4 : thm =
|- !(===) Between.
TarskiModel (===) Between
==> (!a q b c. ?x. Between (q,a,x) /\ a,x === b,c)

That says that ===  is a 2-ary predicate parsed-as-infix defined on ordered pairs and Between is a predicate
defined on ordered triples.  Then TarskiModel is a 2-ary predicate  defined on any such === and Between, and
the predicate is true iff !a q b c. ?x. Between (q,a,x) /\ a,x === b,c, i.e. if Tarski's 4th axiom holds for ===
and Between.  I'm a bit puzzled here because in the statement of A4, I wrote
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
To me, that means that all 7 arguments of === and Between have the same type, the unspecified type 'a, but you
can't see that in val A4 above.  I had the impression that HOL Light printed out less information in the
theorem statements than I'd put in because of its clever type-inference scheme, but this looks like
taking it too far.  Maybe I don't know what 'a means.

--
Best,
Bill

horizon := 0;;

parse_as_infix("===",(12, "right"));;

let A1_DEF = new_definition
A1axiom (===) Between  <=>  !a b. a,b === b,a;;

let A2_DEF = new_definition
A2axiom (===) Between  <=>  !a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s;;

let A3_DEF = new_definition
A3axiom (===) Between  <=>  !a b c. a,b === c,c ==> a = b;;

let A4_DEF = new_definition
A4axiom (===) Between  <=>  !a q b c. ?x. Between(q,a,x) /\ a,x === b,c;;

let TarskiModel_DEF = new_definition
TarskiModel (===) Between  <=>
A1axiom (===) Between /\ A2axiom (===) Between /\ A3axiom (===) Between /\ A4axiom (===) Between;;

let A1 = thm ;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
let a b be 'a;
thus TarskiModel (===) Between  ==>  a,b === b,a
by TarskiModel_DEF, A1_DEF;;

let A2 = thm ;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
let a b p q r s be 'a;
thus TarskiModel (===) Between  ==>  a,b === p,q /\ a,b === r,s ==> p,q === r,s
by TarskiModel_DEF, A2_DEF;;

let A3 = thm ;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
let a b c be 'a;
thus TarskiModel (===) Between  ==>  a,b === c,c ==> a = b
by TarskiModel_DEF, A3_DEF;;

let A4 = thm ;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a q b c be 'a;
thus ?x. Between(q,a,x) /\ a,x === b,c
by TM, TarskiModel_DEF, A4_DEF;;

let EquivReflexive = thm ;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a b be 'a;
thus a,b === a,b

proof
b,a === a,b by A1, TM;
qed by -, A2, TM;;

let EquivSymmetric = thm ;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a b c d be 'a;
assume a,b === c,d [ab_cd];
thus c,d === a,b

proof
a,b === a,b by EquivReflexive, TM;
qed by -, ab_cd, A2, TM;;

let EquivTransitive = thm ;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a b p q r s be 'a;
assume a,b === p,q [H1];
assume p,q === r,s [H2];
thus a,b === r,s

proof
p,q === a,b by H1, EquivSymmetric, TM;
qed by -, H2, A2, TM;;

let Baaa_THM = thm ;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a b be 'a;
thus Between (a,a,a) /\ a,a === b,b

proof
consider x such that
Between (a,a,x) /\ a,x === b,b [useA4] by A4, TM;
a = x by -, A3, TM;
qed by -, useA4;;

let Baaa_THM = thm ;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a b be 'a;
thus Between (a,a,a) /\ a,a === b,b

proof
?x. Between(a,a,x) /\ a,x === b,b by A4, TM;
consider x such that
Between (a,a,x) /\ a,x === b,b [useA4] by -;
a = x by -, A3, TM;
qed by -, useA4;;

let Baaa_THM = thm ;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a b be 'a;
thus Between (a,a,a) /\ a,a === b,b

proof
consider x such that
Between (a,a,x) /\ a,x === b,b [useA4] by A4, TM;
a = x by -, A3, TM;
qed by -, useA4;;

let Bqaa_THM = thm ;
let === be 'a#'a->'a#'a->bool;
let Between be 'a#'a#'a->bool;
assume TarskiModel (===) Between [TM];
let a q be 'a;
thus Between(q,a,a)

proof
consider x such that Between(q,a,x) /\ a,x === a,a [useA4] by A4, TM;
a = x by -, A3, TM;
qed by -, useA4;;

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

5 Aug 2012 14:11

### Re: rigorous axiomatic geometry proof in HOL Light

On 5/08/12 8:49 PM, Bill Richter wrote:

> parse_as_infix("cong",(12, "right"));;

> let cong_DEF = new_definition a,b,c cong x,y,z <=> a,b === x,y /\
> a,c === x,z /\ b,c === y,z;;

> My problem, I think, is that cong is now a function of ===, which is
> now a variable being passed around.  Here's my miz3 code below, which
> I really enjoyed writing, as it took quite a bit of fiddling to get
> right.

Yes, cong needs to take === as a parameter, which probably then means
that you can't have cong as an infix.

You'd have to define

cong R (a,b,c) (x,y,z) <=>
R (a,b) (x,y) /\ R (a,c) (x,z) /\ R (b,c) (y,z)

(where I've replaced === with R just to make everything clearly a variable)

I know how I'd hack the now-parameterised cong into behaving like an
infix thing in HOL4, but I'm not sure how to do it in HOL Light.  You're
definitely butting up against the limits of what is friendly.  (Of
course, you'd like to either have a particular === as an understood
parameter, or to be able to write

(a,b,c) cong_{===} (x,y,z)

or both.

> I'm a bit puzzled here because in the statement of A4, I wrote let
> === be 'a#'a->'a#'a->bool; let Between be 'a#'a#'a->bool; To me, that
> means that all 7 arguments of === and Between have the same type, the
> unspecified type 'a, but you can't see that in val A4 above.  I had
> the impression that HOL Light printed out less information in the
> theorem statements than I'd put in because of its clever
> type-inference scheme, but this looks like taking it too far.  Maybe
> I don't know what 'a means.

In SML and HOL4, 'a is a type variable, not an actual type.  However,
having seen your other scripts, I'm reminded that convention (at least)
allows HOL Light to use capital letters as type variables.   Thus you
earlier wrote

let v be A ..

That capital A is the HOL Light idiom for writing 'a, so you should
stick with it and write

let Between be A#A#A->bool ...

and avoid the 'a.

I'm sorry

type_of MAP

was so unilluminating.  Note that you also earlier confused "map", an
OCaml function and MAP, the logical constant within HOL.  When you
wrote map into the HOL Light interactive loop, it parsed it as a
polymorphic variable because there is no such constant in HOL Light.
(HOL4 shares the common ancestry here; we also have MAP in the logic and
map in the ML system.)

Best,
Michael


------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

6 Aug 2012 07:01

### Re: rigorous axiomatic geometry proof in HOL Light

Thanks, Michael, I'll try out your cong trick.  Your type_of MAP;; was plenty illuminating, that's how I
figured out what polymorphism meant, with the Scheme analogy, but I'm confused.  On p 350 of
http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf
it explains lower-case map:
map : ('a -> 'b) -> 'a list -> 'b list
Are you saying this is an Ocaml function, and not something we can use in HOL Light?  A few pages later is
MAP_EVERY : ('a -> tactic) -> 'a list -> tactic
That certainly sounds like HOL Light.  There is no MAP in reference.pdf.  This brings up a question Colin
Rowat was asking earlier: if you define various vector-related functions in HOL Light (like the maximum
of a vector, or the dot product of two vectors...), how can you check if your code is working?  Is there some
cooperation between ML and HOL that I'm missing?  Obviously HOL is coded up in ML, but are you supposed to mix
freely ML and HOL code somehow?

--

--
Best,
Bill

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

3 Aug 2012 08:54

### Re: rigorous axiomatic geometry proof in HOL Light

On Fri, Aug 3, 2012 at 4:43 AM, Bill Richter wrote:
Define a four-argument predicate
Hilbert_plane H (Between) (===) Line = axiom_1_holds /\ axiom_2_holds /\
...
and use that as a hypothesis on all your theorems.

Thanks, Ramana!  The code below indicates that I can get rid of new_axiom following your suggestion.  I should have seen this myself before, but I was bogged down in the set theory which I still don't know how to pull off, so I didn't even try.  So thanks!

I kept the new_type stuff, and made TarskiModel a 0-argument predicate, and proved the first 4 theorems of my Tarski axiomatic geometry http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml

EquivReflexive : thm = |- TarskiModel ==> (!a b. a,b === a,b)
EquivSymmetric : thm =
|- TarskiModel ==> (!a b c d. a,b === c,d ==> c,d === a,b)
EquivTransitive : thm =
|- TarskiModel
==> (!a b p q r s. a,b === p,q ==> p,q === r,s ==> a,b === r,s)
Baaa_THM : thm =
|- TarskiModel ==> (!a b. Between (a,a,a) /\ a,a === b,b)

I'm not too happy about the extra clutter caused by the statement TarskiModel, the label TM I use to refer to it, and turning the axioms into theorems.  But that's great that I can get rid of new_axiom at least, so thanks.

If HOL Light has record datatypes (not sure if it does), you can at least hide all the arguments to TarskiModel inside a record. And put an overload of TM for TarskiModel so you don't have to type/read the long name everywhere. (Come to think of it, overloads may also not be available in HOL Light...)

In HOL4 you could use both features I mention above.

In Isabelle, you could do the whole thing much more cleanly using what is known as a "locale", where you fix some constants like ===, Between, H, etc. and state some properties (the axioms) you want to hold of them in this context, and then do your formalisation without the clutter, and at the end it gives you the effect of having used the extra hypothesis on every theorem.

(All these features could exist in all the theorem provers; they just happen not to.)

Finally, if you go back to your old new_axiom way in HOL Light for convenience, it may be possible to simulate locales by using OpenTheory theory packages. But I can't really recommend that yet because the idea is completely untested.

I don't know how to get rid of new_type using H and your 4-arg predicate.   I tried this, and I got the error message
#     Exception: Failure "term after binary operator expected":

parse_as_infix("===",(12, "right"));;
let A1_DEF = new_definition
A1axiom  T  ===  <=>  !a b. T a /\ T b  ==>  a,b === b,a;;

I can appreciate this error message.  I want to say that T is a set and a belongs to T (or T a = True, or T a), but I don't see how I can do that without some typing.  What do I even want the type of a, b & T to be here?

This seems to be a question of how to implement sets in HOL Light.

--
Best,
Bill

horizon := 0;;

new_type("point",0);;
new_constant("===",:point#point->point#point->bool);;
new_constant("Between",:point#point#point->bool);;

parse_as_infix("===",(12, "right"));;

let A1_DEF = new_definition
A1axiom  <=>  !a b. a,b === b,a;;

let A2_DEF = new_definition
A2axiom  <=>  !a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s;;

let A3_DEF = new_definition
A3axiom  <=>  !a b c. a,b === c,c ==> a = b;;

let A4_DEF = new_definition
A4axiom  <=>  !a q b c. ?x. Between(q,a,x) /\ a,x === b,c;;

let TarskiModel_DEF = new_definition
TarskiModel  <=>  A1axiom /\ A2axiom /\ A3axiom /\ A4axiom;;

let A1 = thm ;
TarskiModel  ==>  !a b. a,b === b,a
by TarskiModel_DEF, A1_DEF;;

let A2 = thm ;
TarskiModel  ==>  !a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s
by TarskiModel_DEF, A2_DEF;;

let A3 = thm ;
TarskiModel  ==>  !a b c. a,b === c,c ==> a = b
by TarskiModel_DEF, A3_DEF;;

let A4 = thm ;
TarskiModel  ==>  !a q b c. ?x. Between(q,a,x) /\ a,x === b,c
by TarskiModel_DEF, A4_DEF;;

let EquivReflexive = thm ;
TarskiModel  ==> !a b. a,b === a,b

proof
assume TarskiModel [TM];
let a b be point;
b,a === a,b by A1, TM;
qed by -, A2, TM;;

let EquivSymmetric = thm ;
assume TarskiModel [TM];
let a b c d be point;
assume a,b === c,d [1];
thus c,d === a,b

proof
a,b === a,b by EquivReflexive, TM;
qed by -, 1, A2, TM;;

let EquivTransitive = thm ;
assume TarskiModel [TM];
let a b p q r s be point;
assume a,b === p,q [H1];
assume p,q === r,s [H2];
thus a,b === r,s

proof
p,q === a,b by H1, EquivSymmetric, TM;
qed by -, H2, A2, TM;;

let Baaa_THM = thm ;
assume TarskiModel [TM];
let a b be point;
thus Between (a,a,a) /\ a,a === b,b

proof
consider x such that
Between (a,a,x) /\ a,x === b,b [X1] by A4, TM;
a = x by -, A3, TM;
qed by -, X1;;

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

5 Aug 2012 09:18

### Re: rigorous axiomatic geometry proof in HOL Light

Thanks, Ramana!  I've often wanted Isabelle locales.  Are you going to code them in HOL4?  For readability I'd
like to not "constantly have this annoying TarskiModel hypothesis hanging around," as Michael said, but
it would be good to write up a longer version of at least part of my code to show that I can avoid both new_axiom
and new_type.

Does you folks know about the Coq work of Vladimir Voevodsky, a mathematician with a Fields medal?
Vladimir is even in my subject, homotopy theory, although I don't understand any of his.  He says he's
working on "new foundations of mathematics", although to my untutored eye, he seems to be formalizing
homotopy theory:

My feeling is that Vladimir's work is a sign that mathematicians and CS folks ought to work together on
formal proofs.  With this in mind, here are a few dumb questions and points:

Why are there so many HOLs, HOL Light, Hol4, Holzero?  Why don't you all work on the same program?  It kinda
seems that HOL4 is the theoreticians and John racks up the theorems.   That sounds like a good combination to
me!  Are you exploring different theoretical possibilities?

It sure seems to me that "Working in a Model of ZFC" is more descriptive than HOL.  Since working in a model is
soooo much more pleasant than strict syntactic FOL proofs, that explains why HOL is more pleasant than
FOL, but it doesn't justify the terminology.  Maybe I'm missing something.

Why are miz3 and Mizar the only proof assistants where one can easily write up human readable proofs?  Why
can't you write readable declarative proofs in every proof assistant, e.g. HOL4?  I'd be happy to port my
code to HOL4 or Isabelle if I knew how to write human readable proofs there.

Michael seemed to suggest earlier that miz3 was intentionally weakened, and I see no evidence of this.  It
could be that Mizar is intentionally weak (I've read this is a feature in using Mizar to teach classes), and
there are Mizar documents I've been told about, but I really don't care about Mizar.  Mizar was a great
pioneering effort in human readable proofs, but I don't think Mizar is really part of the formal proofs
revolution.  Freek's code miz3.ml I think just sets up the format for miz3 code, caching proofs, mixing
declarative and procedural, all very impressive hard work, and I've found no bugs.  The labor of "by"
calculations is done in John's Examples/holby.ml, and it's hard to believe that John would have
intentionally weakened his own attempt!   I found no evidence of intention
ally weakening.  Freek, Cris and Rob got me to understand that miz3 is a lot more powerful than I thought.
Holby.ml does some simple things and then calls MESON, which has a built-in depth!
limit of 50 (I don't know what that means), and MESON only does FOL, not HOL (don't quite get that either).  How
much weakness do these two facts explain?   Could we substitute some other prover for MESON to increase the
power of miz3?

If someone could look at my 3500 lines of miz3 Hilbert axiomatic geometry code
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
they could maybe explain what MESON isn't doing because it's FOL.  My unlearned opinion is that my Hilbert
code uses real HOL, because there I use so much sets (from sets.ml), but my Tarksi code
http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml
only uses FOL, and therefore MESON should do a better job on my Tarski code than my Hilbert code. But this is
just wild speculation on my part.

From skimming your sources very superficially, it looks as if the
Between 'constant' would need to be a parameter of TarskiModel too.

Thanks, Michael!  I think I'll have to learn what polymorphism means before I can grok your post.  There ought
to be examples in the HOL dox of how to define common complicated set-theoretic structures that come up in
math all the time.  In math one just says

A Tarski plane in a set T together with subsets
Between subset T^3
Equiv subset T^4
satisfying these 11 axioms.

A Hilbert plane H is more complicated, because of congruence being defined not on points but subsets of H.
P(X)
called the open sets of X, satisfying various properties.

If you read something saying that there is no empty set, it's
meaning that there is no empty type.

Thanks, Michael, that helps a lot!   I definitely missed that.  I'm just on page 1 (actually 9) of your Logic manual:

This model is given in terms of a fixed set of sets U, which will be
called the universe and which is assumed to have the following
properties.
Inhab Each element of U is a non-empty set.

I would have thought that U here is a "universe", the set of sets that we're going be allowed to use.  However,
this paragraph begins with

The HOL syntax contains syntactic categories of types and terms
whose elements are intended to denote respectively certain sets and
elements of sets.

I guess I can't even read that.   Does that say that an element of a type is a set (or element of a set)?   And does
that mean that U is not the universe of sets, but instead, the "universe" of types?  Shows you what you get
from just reading the first page!  If I read the whole manual, or even the first chapter, I'd probably understand.

--

--
Best,
Bill

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

5 Aug 2012 13:25

### Re: rigorous axiomatic geometry proof in HOL Light


On 5 Aug 2012, at 08:18, Bill Richter wrote:

> Thanks, Ramana!  I've often wanted Isabelle locales.  Are you going to code them in HOL4?

Locales are one of the many things that (I believe) make the Isabelle HOL logic much more bloated than the
original and best HOL logic as supported by HOL4, HOL Light, HOL Zero and ProofPower. It might be possible
to give a similar facility as a bolt-on outside the logic.

>  For readability I'd like to not "constantly have this annoying TarskiModel hypothesis hanging around,"
as Michael said, but it would be good to write up a longer version of at least part of my code to show that I can
avoid both new_axiom and new_type.
>
> Does you folks know about the Coq work of Vladimir Voevodsky, a mathematician with a Fields medal?

> Vladimir is even in my subject, homotopy theory, although I don't understand any of his.  He says he's
working on "new foundations of mathematics", although to my untutored eye, he seems to be formalizing
homotopy theory:
>

People who don't know about Voevodsky's ideas may like to watch the videos of two interesting talks by him:

http://video.ias.edu/voevodsky-80th

http://video.ias.edu/conversations/voevodsky#attachments

> My feeling is that Vladimir's work is a sign that mathematicians and CS folks ought to work together on
formal proofs.  With this in mind, here are a few dumb questions and points:
>
> Why are there so many HOLs, HOL Light, Hol4, Holzero?

That's a very long story. HOL4 and ProofPower came first in the early 90s as a result of roughly simultaneous
efforts in academia (HOL4) and industry (ProofPower) to port Mike Gordon's original Classic HOL onto
Standard ML. John wrote HOL Light a few years later, see
http://www.cl.cam.ac.uk/~jrh13/papers/holright.html for some of his motivation. Holzero is much
more recent work by Mark Adams and Mark's website explains his rationale. There is also HOL Omega by Peter
Homeier, which is an extension of HOL4 to support quantification over types.

>  Why don't you all work on the same program?

My reason for sticking with ProofPower is that I know it and that, until recently, it was the only HOL that
offered civilised logical and mathematical notation (foralls and exists and cups and caps etc.) on
screen. ProofPower also encourages you to make nice LaTeX documents out of your specifications and proofs.

>  It kinda seems that HOL4 is the theoreticians and John racks up the theorems.

>   That sounds like a good combination to me!  Are you exploring different theoretical possibilities?
>

I don't see it like that. I would say that HOL4 is better documented than HOL Light and has a lot more library
support for system verification. That said, HOL Light is much better documented now than it was in the
past. HOL4 is probably the system of choice for people doing research in hardware or software
verification, while HOL Light has got a lot more support for mathematics.

> It sure seems to me that "Working in a Model of ZFC" is more descriptive than HOL.  Since working in a model is
soooo much more pleasant than strict syntactic FOL proofs, that explains why HOL is more pleasant than
FOL, but it doesn't justify the terminology.  Maybe I'm missing something.
>

Actually, in HOL you are working in a model of Zermelo set theory with choice, not ZFC - there is nothing
equivalent to the axiom of replacement in HOL. I agree that saying that we work in polymorphic typed set
theory gives a better idea of the actual mathematical experience than saying it is higher-order logic.

> Why are miz3 and Mizar the only proof assistants where one can easily write up human readable proofs?  Why
can't you write readable declarative proofs in every proof assistant, e.g. HOL4?

I would say it is because the community has put far more effort into tools that make it easier to find proofs
and because proof automation conflicts with the desire for proof scripts that are readable on their own.
For many of us, a long-term goal is to provide tools that can outstrip human capability on useful classes of
problems. We can already do this in some cases, e.g., calculating derivatives. If the tool can calculate
something for me, why should I have to write down the result of the calculation?

Readability of a proof on its own rather than comprehensibility of the proof when you replay it and see what
happens is a non-trivial research topic in its own right. I see it as quite problematic. For a start,
readability depends on the reader. Very often an expert will be happy with a few strategic pointers while a
beginner wants lots of detail, so they need to see different projections of the proof.

Personally, I find Mizar proofs unreadable. Or rather I have never learnt how to read them and don't feel
greatly motivated to do so.

> ...
> Thanks, Michael!  I think I'll have to learn what polymorphism means before I can grok your post.

In a typed system, polymorphism gives you the ability to formalise a concept like "set union" as a single
object "cup" that works for sets of any type, providing the types agree. For example, all the HOLs have
distinct types for natural numbers and for real numbers. Without polymorphism, you would need to define
distinct functions for all the types you were interested in:

nat_cup : nat SET -> nat SET -> nat SET
real_cup : real SET -> real SET -> real SET
nat_pair_cup (nat x nat) SET -> (nat x nat) SET -> (nat x nat) SET

etc. With polymorphism you define:

cup : 'a SET -> 'a SET -> 'a SET

where "'a" is a so-called type variable. cup then works as if it has every type of the form "t SET -> t SET -> t SET".

>  There ought to be examples in the HOL dox of how to define common complicated set-theoretic structures
that come up in math all the time.  In math one just says
>
> A Tarski plane in a set T together with subsets
> Between subset T^3
> Equiv subset T^4
> satisfying these 11 axioms.
>
> A Hilbert plane H is more complicated, because of congruence being defined not on points but subsets of H.
> P(X)
> called the open sets of X, satisfying various properties.

You may be interested in my ProofPower development of a little bit of elementary topology. See:

http://www.lemma-one.com/ProofPower/examples/wrk067.pdf

You will see there how polymorphism can obviate the clunky distinction between classes and sets that one
gets when working in first-order set theory. I define a polymorphic set 'a Topology as the set of all
topologies with points of type 'a. This is then a first-class object representing the class of all
topological spaces.

>
>   If you read something saying that there is no empty set, it's
>   meaning that there is no empty type.
>
> Thanks, Michael, that helps a lot!   I definitely missed that.  I'm just on page 1 (actually 9) of your Logic manual:
>
>   This model is given in terms of a fixed set of sets U, which will be
>   called the universe and which is assumed to have the following
>   properties.
>   Inhab Each element of U is a non-empty set.
>
> I would have thought that U here is a "universe", the set of sets that we're going be allowed to use.  However,
this paragraph begins with
>
>   The HOL syntax contains syntactic categories of types and terms
>   whose elements are intended to denote respectively certain sets and
>   elements of sets.
>
> I guess I can't even read that.   Does that say that an element of a type is a set (or element of a set)?

It means that types denote sets and terms denote elements.  Each term has a unique type and is guaranteed to
denote an element of the set denoted by that type.

(When you write down a term in the concrete syntax, you don't have to write down all the type information
associated with it. The tool infers a most general possible type for the term and uses that. Abstractly and
in the underlying represention used in the tool, all the type information is there in the term.)

>  And does that mean that U is not the universe of sets, but instead, the "universe" of types?

The denotations of types range over U and the denotations of terms range over \bigcup U.

> Shows you what you get from just reading the first page!

>  If I read the whole manual, or even the first chapter, I'd probably understand.
>

The definition of the closure properties required of U finish on the top of the second page!

Regards,

Rob.

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

5 Aug 2012 22:01

### Re: rigorous axiomatic geometry proof in HOL Light

On Sun, Aug 5, 2012 at 12:25 PM, Rob Arthan <rda <at> lemma-one.com> wrote:
>
> On 5 Aug 2012, at 08:18, Bill Richter wrote:
>
>> Thanks, Ramana!  I've often wanted Isabelle locales.  Are you going to code them in HOL4?
>
> Locales are one of the many things that (I believe) make the Isabelle HOL logic much more bloated than the
original and best HOL logic as supported by HOL4, HOL Light, HOL Zero and ProofPower. It might be possible
to give a similar facility as a bolt-on outside the logic.

I think everyone agrees that locales _can_ be extra-logical. I was
also under the impression that they _are_ that way in Isabelle/HOL.
(This is in contrast to axiomatic type classes, which are in
Isabelle's logic from Pure upwards.) Anyone who knows better about
locales as implemented in Isabelle, correct me if I'm wrong.

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

5 Aug 2012 15:35

### Re: rigorous axiomatic geometry proof in HOL Light

On Sun, 5 Aug 2012, Rob Arthan wrote:

>> I've often wanted Isabelle locales.  Are you going to code them in
>> HOL4?
>
> Locales are one of the many things that (I believe) make the Isabelle
> HOL logic much more bloated than the original and best HOL logic as
> supported by HOL4, HOL Light, HOL Zero and ProofPower. It might be
> possible to give a similar facility as a bolt-on outside the logic.

Locales are not even part of Isabelle/HOL, but of Isabelle/Pure, where
they are added as an infrastructure outside the logic.  (Most of
Isabelle/Pure is just infrastructure in some sense.)

Historically it were the Coq guys who made their "sections" part of the
core logic, and regretted it ever after.  Today they follow a more HOL-ish
approach: Coq type classes are merely some infrastructure around the
logic.

More historically, Isabelle type classes were done the other way round: as
some kind of kernel extension of Isabelle/Pure, but we also regretted
that.  In recent years we have moved more and more towards rephrasing (and
rebasing) type classes in terms of locales, and thus outside the logic.
This is still not fully achieved.

Anyway, I've asked myself the same question above, when some HOL person
will start to implement a version of "sections" or "locales".  My estimate
is that when starting today, it would take approx. 5 years to make this
become real. Our very first version of Isabelle locales can be seen here
(14 years ago):
http://isabelle.in.tum.de/repos/isabelle/file/5313f781efe0/src/Pure/locale.ML

Makarius

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

6 Aug 2012 02:11

### Re: rigorous axiomatic geometry proof in HOL Light

> Anyway, I've asked myself the same question above, when some HOL person
> will start to implement a version of "sections" or "locales".  My estimate
> is that when starting today, it would take approx. 5 years to make this
> become real. Our very first version of Isabelle locales can be seen here
> (14 years ago):
> http://isabelle.in.tum.de/repos/isabelle/file/5313f781efe0/src/Pure/locale.ML
>
>
>         Makarius

My opinion is that Peter Homeier's HOL-Omega is the right setting to
properly implement
something locale-like, since it provides quantification over type
variables in the logic.
In plain old HOL the implementation of locales as essentially assumptions on
goals is too limiting for polymorphism.

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

6 Aug 2012 11:19

### Re: rigorous axiomatic geometry proof in HOL Light

On Sun, 5 Aug 2012, Konrad Slind wrote:

> My opinion is that Peter Homeier's HOL-Omega is the right setting to
> properly implement something locale-like, since it provides
> quantification over type variables in the logic. In plain old HOL the
> implementation of locales as essentially assumptions on goals is too
> limiting for polymorphism.

In the 1.5 decades refining Isabelle locales, we have separated these two
concerns: (1) management of local contexts and definitional specifications
wrt. local contexts, (2) logical foundations for building actual abstract
contexts.

(1) is the infrastructure, consisting of quite a bit of abstract
non-sense.  It is now called "local theory" in Isabelle.  It provides some
interfaces for definitions in a local context, where the results are
polymorphic in the sense of Hindley-Milner, but some types may remain
fixed according to the context.

(2) are concrete implementations of locales, type classes, type-class
concepts for modular theories using facilities of HOL-Omega, or external
theory interpretation as in Isabelle/AWE from Bremen.

Both (1) and (2) are difficult to implement.  We are still working on
various fine points concerning local syntax (via notation or abbreviation)
that moves between such local contexts.  Another challenge that I have
boldly revisited this year is to allow nesting of locale-like contexts.

What is also difficult to get right are declarations for proof tools
associated with theorems produced in abstract situations, when they start
moving around to other contexts.  E.g. ways to manage "simpset"-like
containers in conformance to abstract theories and their interpretations
by concrete instances.

Type classes have turned out an important special case for all that,
because the abstraction looks "concrete", via polymorphic constants with
some specific type constraints.  Syntax and tool declarationas are often
stable wrt. type-instantiation of class constants, without further ado.

Makarius

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

6 Aug 2012 06:43

### Re: rigorous axiomatic geometry proof in HOL Light

Cris, the axiom of choice is essential in much of modern math, and I'm guessing that's John's reason.

Rob, that was a very interesting post, which I can't do justice too.  I would be very interested if you say
you how to port it to HOL Light.  Did you say that ProofPower has Isabelle-type fonts (foralls and exists and
cups and caps etc.)?  I have those myself in HOL-Light, and John approved of my Emacs pre-processor style,
as you'll see if you read my code, now with a very nice proof of Euclid's Prop I.7, of which Hartshorne gave an
incomplete proof
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
EuclidProp7_THM : thm =
|- !A B C D a.
~(A = B)
==> Line a /\ A IN a /\ B IN a
==> ~(C = D) /\ C NOTIN a /\ D NOTIN a /\ C,D same_side a
==> seg A C === seg A D
==> ~(seg B C === seg B D)

If you can't read Mizar proofs, maybe I'm your man.  I'm sure you can read the miz3 proofs I coded for your proof
of Los's Logic problem.  I can't believe you'd have any trouble reading my miz3 Hilbert code above.   I
heartily dislike the Mizar type system and the Mizar vocabulary biz.   Perhaps we're not talking about the
same thing.  To understand Mizar or miz3 well enough to code it yourself is very different from merely being
able to read  proofs others wrote.  Thanks for clarifying HOL4, ZFC vs ZC, and I have to set this off, it sounds
so cool:  Instead of HOL, we should call it

polymorphic typed set theory

The overwhelming advantage of readable proofs is that CS folks and mathematicians can work together on
formal proofs.  Isn't that a great team?  I certainly think so, because the CS folks are the ones who are good
at computers.  I think John answers your questions about "tools that can outstrip human capability" in the
interactive chapter of his purple book.  Basically, I think, he says that neither of the two approaches
(get the computer to do it, or write up the proof in full yourself) is that powerful, so they should be mixed
together.  As John thanks you (and Michael etc) for help, maybe you make a reply here.

--

--
Best,
Bill

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

23 Aug 2012 01:06

### Re: rigorous axiomatic geometry proof in HOL Light


Rob wrote:

| > Why are there so many HOLs, HOL Light, Hol4, Holzero?
|
| That's a very long story. HOL4 and ProofPower came first in the early
| 90s as a result of roughly simultaneous efforts in academia (HOL4) and
| industry (ProofPower) to port Mike Gordon's original Classic HOL onto
| Standard ML. John wrote HOL Light a few years later, see
| http://www.cl.cam.ac.uk/~jrh13/papers/holright.html for some of his
| motivation. Holzero is much more recent work by Mark Adams and Mark's
| website explains his rationale. There is also HOL Omega by Peter
| Homeier, which is an extension of HOL4 to support quantification over
| types.

Well, to be strictly accurate at the cost of an even longer story, it
was a HOL4 precursor called hol90 that was developed by Konrad Slind
contemporaneously with ProofPower, and this evolved via hol98 into
HOL4 some years later in the hands of Michael Norrish together with
Konrad, as well as forming the main starting point for HOL Light. I
have a little slide that I sometimes use in talks showing my picture
of the HOL family tree. See, for example, slide 30 of the following:

http://www.cl.cam.ac.uk/~jrh13/slides/popl-28jan11/slides.pdf

I would also add HOL2P (http://cswww.essex.ac.uk/staff/norbert/hol2p/)
to the list of broadly upward-compatible extensions to the HOL logic.
>From an implementation point of view, HOL2P is a HOL Light extension
while HOL-Omega is a HOL4 extension. From a logical point of view,
HOL-Omega is, as I understand it, a further generalization of HOL2P,
which is itself a generalization of HOL.

John.

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

7 Aug 2012 14:19

### Re: rigorous axiomatic geometry proof in HOL Light

Hi Bill,

>Why are miz3 and Mizar the only proof assistants where
>one can easily write up human readable proofs?

I'm surprised you're not including Isar in this list!

And do you know about ForTheL (see

Also, does anyone know what is the status of Mohan
Ganesalingam's work in this direction (see for example
<http://people.pwf.cam.ac.uk/mg262/CSLI%20talk.pdf>)?

Freek

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/

7 Aug 2012 14:58

### Re: rigorous axiomatic geometry proof in HOL Light

On Tue, Aug 7, 2012 at 1:19 PM, Freek Wiedijk <freek <at> cs.ru.nl> wrote:
> Also, does anyone know what is the status of Mohan
> Ganesalingam's work in this direction (see for example
> <http://people.pwf.cam.ac.uk/mg262/CSLI%20talk.pdf>)?

No, but we can ask him :) (CC'ed)
Context: http://sourceforge.net/mailarchive/message.php?msg_id=29635641,
http://sourceforge.net/mailarchive/message.php?msg_id=29644387.
By the way, the page one level up, http://people.pwf.cam.ac.uk/mg262/,
has his thesis and other good stuff.

>
> Freek
>
> ------------------------------------------------------------------------------
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> _______________________________________________
> hol-info mailing list
> hol-info <at> lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
`

Gmane