So I now finally understand that no-tactics miz3 can be used as a
theorem-prover, but that I was not doing so: miz3 and MESON won't try to prove
anything except my statements
x by th1, th2, ...
and only by trying to build a FOL proof of the implication
th1 /\ th2 /\ th3 ... ==> x
then as long as my statements `x by th1, th2, ...' seem obvious to me, I run
only a very minor risk of miz3 doing something really smart that I don't
understand. That's great, and thanks to everyone for helping me understand
this.
I'm curious about using no-tactics miz3 or any other proof assistant to produce
1-line proofs, though. I'm not doing very well with miz3, and I suppose
that's a good thing. I set the timeout pretty high
timeout := 4000;;
and I timed out (on an old slow machine) at 18 & 26 million in trying to
convert some pretty simple proofs to 1-line proofs (original proofs commented
out):
let Line01infinity_THM = thm `; :: #2 timeout at 18,678,485
let X be point;
let l m be point_set;
assume Line l /\ Line m [H0];
assume ~(l = m) [H1];
assume X IN l /\ X IN m [H2];
thus l INTER m = {X}
:: proof
:: assume ~(l INTER m = {X}) [H3];
:: X IN l INTER m by H2, IN_INTER;
:: consider A such that
:: A IN l INTER m /\ ~(A = X) [X1] by -, H3, BiggerThanSingleton_THM;
:: A IN l /\ X IN l /\ A IN m /\ X IN m by H0, -, H2, IN_INTER;
:: l = m by H0, -, X1, I1;
:: F by -, H1;
:: qed by -
by H0, H1, H2, IN_INTER, BiggerThanSingleton_THM, I1`;;
let SameSideLinesIntersect1Point_THM = thm `; :: #2 timeout at 26,338,897
let A B X be point;
let l m be point_set;
assume Line l /\ Line m [H0];
assume l INTER m = {X} [H1];
assume A IN m DELETE X /\ B IN m DELETE X [H2];
assume ~(A,B same_side l) [H3];
thus A NOTIN l /\ B NOTIN l /\ X IN open (A,B)
:: proof
:: A NOTIN l /\ B NOTIN l [notABl] by H1, H2, EquivIntersectionHelp_THM;
:: A IN m /\ B IN m /\ ~(A = X) /\ ~(B = X) [H2'] by H2, IN_DELETE;
:: ~(open (A,B) INTER l = {}) [nonempty] by H0, H3,
SameSideDisjointIntersection_THM;
:: open (A,B) SUBSET m [ABm] by H0, H2', OpenIntervalSubsetLine_THM;
:: open (A,B) INTER l SUBSET {X} by -, SubsetTensor_THM, H1, INTER_COMM;
:: X IN open (A,B) INTER l by nonempty, -, NonemptySubsetSing_THM;
:: qed by notABl, -, IN_INTER
by H0, H1, H2, H3, EquivIntersectionHelp_THM, IN_DELETE,
SameSideDisjointIntersection_THM, OpenIntervalSubsetLine_THM, SubsetTensor_THM,
INTER_COMM, NonemptySubsetSing_THM, IN_INTER`;;
I think everyone will agree that these two results look pretty obvious.
Line01infinity_THM says that if a point X belongs to two lines distinct l and
m, then l INTER m = {X}. That's just axiom I1, two points determine a line.
The next result says that if l INTER m = {X} and points A, B on m are on
opposite sides of l, then X must be between A and B. If MESON can't prove
that in 26 million whatevers, then I think I agree with Ramana and Michael that
MESON isn't the top FOL prover. I bet I could do a lot better if I learned how
to use HOL tactics. I'm interested in seeing if some better FOL prover would
verify such 1-line proof versions of most of my result.
Josef, let me try again. I apologize for not knowing the terminology or
anything about Vampire. Would there be a way to turn my 971 lines of Tarski
code http://www.math.northwestern.edu/~richter/TarskiAxiomGeometryCurry.ml
(which for Freek I made all my predicates official curried HOL functions, in
order to show that holby is weaker than Mizar) into say 150 lines of 1-line
proofs that a top FOL prover would then verify? I think you did something
like, but don't have the 150 line file.
--
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
