I've now formalized all the theorems in the first 6 sections of my Hilbert
axiomatic geometry paper http://www.math.northwestern.edu/~richter/hilbert.pdf
in 2800 lines of miz3 code
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
My last result was Moise and Venema's Plane Separation axiom:
Prop 4.13: The complement in the plane of a line l is a disjoint union
of two nonempty convex sets H1 and H2. If P ∈ H1 and Q ∈ H2 , then
¬(open (P,Q) ∩ l = ∅).
It's easy mathematically but used a lot of HOL set theory. I'm very
happy to have formalized it, and I'm including the defs & thms below.
Ramana, I think my definition of power is quite different from any of your 3
definitions. I thought my last post was clear, but maybe it wasn't. Let me
try again: I want to say that miz3 (without tactics) is so lacking in power
that a human can read such miz3 proofs. I think if anyone read my code, they
could understand quite as easily as my paper. I want to say that in such a
miz3 line
alpha by X1, X2, ..., Xn;
which miz3 says is OK, that a human will easily be able to check that results
X1,..., Xn actually prove alpha. Provided that the human understands alpha,
X1,...,Xn, of course. I think this lack of power can be explained precisely
with some kind of an upper bound.
Now I believe that MESON is much more powerful than that. I think we can all
be astounded by what MESON can prove for us. But I don't believe that miz3
(without tactics) uses the full power of MESON.
--
Best,
Bill
PlaneComplement_DEF : thm =
|- ∀ P A α. complement α P ⇔ P ∉ α
CONVEX : thm =
|- ∀α. Convex α ⇔
(∀ A B. A ∈ α ∧ B ∈ α ⇒ open (A,B) ⊂ α)
HalfPlaneConvexNonempty_THM : thm =
|- ∀l H A.
Line l ∧ A ∉ l ∧
(∀X. X ∈ H ⇔ X ∉ l ∧ X,A same_side l)
⇒ ¬(H = ∅) ∧ H ⊂ complement l ∧ Convex H
PlaneSeparation_THM : thm =
|- ∀ l. Line l
⇒ (∃ H1 H2.
H1 ∩ H2 = ∅ ∧ ¬(H1 = ∅) ∧ ¬(H2 = ∅) ∧
Convex H1 ∧ Convex H2 ∧ complement l = H1 ∪ H2 ∧
(∀P Q. P ∈ H1 ∧ Q ∈ H2 ⇒ ¬(P,Q same_side l)))
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
