Hi Bill,
| But I don't like that plan, and I think you don't either. I think we
| think that HOL can easily be tweaked to give axiomatic geometry proofs
| that are just as readable as my Mizar proofs. How do we get started
| working on this? I can't yet use any mizar mode in HOL Light, and
| maybe because I can only build an old version 3.09.
I have just tried things out myself with OCaml 3.09.2, and everything
seemed all right. Can you tell me what goes wrong when you try to
follow the instructions in my earlier message for running Mizar modes?
Once you get a Mizar mode working, I don't think it's difficult to
translate your proofs into any of them. For example, continuing the
little fragment I sent before where I set up some of the axioms,
here are miz3 versions of your first few proofs, which look fairly
similar to the originals:
loadt "miz3/miz3.ml";;
let EquivReflexive = thm `;
!a b. a,b === a,b
proof
let a b be Plane;
b,a === a,b by AXIOM_1;
thus a,b === a,b by AXIOM_2;
end`;;
let EquivSymmetric = thm `;
!a b c d. a,b === c,d ==> c,d === a,b
proof
let a b c d be Plane;
assume a,b === c,d [1];
a,b === a,b by EquivReflexive;
thus c,d === a,b by 1, AXIOM_2;
end`;;
let EquivTransitive = thm `;
!a b p q r s : Plane. a,b === p,q /\ p,q === r,s ==> a,b === r,s
proof
let a b p q r s be Plane;
assume a,b === p,q [1];
assume p,q === r,s [2];
p,q === a,b by 1, EquivSymmetric;
thus a,b === r,s by 2, AXIOM_2;
end`;;
let Baaa_THM = thm `;
!a b. Between (a,a,a) /\ a,a === b,b
proof
let a b be Plane;
?x. Between (a,a,x) /\ a,x === b,b by AXIOM_4;
consider x such that Between (a,a,x) /\ a,x === b,b [1];
a = x by 1, AXIOM_3;
thus Between (a,a,a) /\ a,a === b,b by 1;
end`;;
I don't think it would be hard to continue this translation, and
indeed I suspect it could be largely done with a bit of clever
editing. But perhaps first one should pause to get the precise formal
setup exactly the way you want. For example, maybe "Point" would be a
more intuitive name than "Plane" for the underlying type, and you
might want to use the same formulation as in your Mizar where
"TarskiModel" becomes a hypothesis instead of working in a specific
model of the axioms as I've been doing.
| Your article sounded very interesting, but I couldn't find it:
| Szczerba The use of Mizar in a course in foundations of geometry
Yes, it's somewhat obscure, and I don't know how to find it online.
I must have seen the original physical volume somewhere a long time
ago. But there are other papers about Mizar in education that are
easier to locate, e.g. "Mizar as a tool for teaching mathematics" or
"Mizar course in Logic and Set Theory".
| Your geometry links don't seem to jibe well with my paper above.
Well, there are lots of degrees of freedom over how to axiomatize
geometry, what level of automation you want and what your overall
goals are in mechanization and formalization. But in any case, I
just wanted to indicate how you might get started if you do want to
use HOL Light.
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/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
