Thanks again, everyone, and I realized how wrong I was last night and performed Michael's exercise:
What if you quote H1, H2 and all of the theorems that you ultimately quoted in the final proof as arguments to "by"? Does miz3 "by" then get it in one step? That's the true test. Below I reproved my first 23 theorems with 1-line proofs of this sort. Arguably they're all pretty obvious results, although one of them earned a MESON solved at number of 849,716. The computer keeps rebooting on my 24th theorem (I've gotten a partial MESON number of 18million), so I'll report on that later. I see how I've been so wrong about miz3 & MESON. In my Hilbert axiomatic geometry code, I only asked miz3 to verify logical deductions that I thought were obvious. I never asked miz3 to prove the theorems for me. What I didn't ask for, I didn't get! I draw 2 conclusions: 1) Michael is right: miz3 (using MESON) could conceivably justify any miz3 statement x by th1, th2, ... as long as the implication th1 /\ th2 /\ th3 ... ==> x is actually provable in FOL or maybe HOL. If this implication is provable and miz3 gives a #2 timeouts error, that's only because miz3 is preventing itself from trying hard enough to prove this implication. That's the answer to the theoretical question I needed for my paper: x by th1, th2, ... will be verified if it's true and if miz3 thinks it's "easy enough". 2) Thus even non-tactics miz3 can be used to try to prove theorems rather to verify proofs. This doesn't affect my educational scheme of high school student coding up their rigorous axiomatic geometry proofs in miz3. If miz3 verifies a student's proof, and I think the proof is too short, I can ask the student for more details. Math is always like that. Josef, I looked at your code http://bit.ly/KfuypA, and it doesn't look short. Let me ask you again: did you code up short Vampire proofs of my Tarski results, something like the 1-line proofs I have below (after the almost 200 lines of definition and axioms)? -- Best, Bill horizon := 0;; timeout := 1000;; 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`);; parse_as_infix("cong",(12, "right"));; parse_as_infix("same_side",(12, "right"));; parse_as_infix("===",(12, "right"));; parse_as_infix("<_seg",(12, "right"));; parse_as_infix("<_ang",(12, "right"));; parse_as_infix("Suppl",(12, "right"));; parse_as_infix("NOTIN",(11, "right"));; let NOTIN = new_definition `!a:A l:A->bool. a NOTIN l <=> ~(a IN l)`;; let Interval_DEF = new_definition `! A B X. open (A,B) X <=> Between A X B`;; let Collinear_DEF = new_definition `Collinear A B C <=> ? l. Line l /\ A IN l /\ B IN l /\ C IN l`;; let SameSide_DEF = new_definition `A,B same_side l <=> Line l /\ ~(? X. (X IN l) /\ X IN open (A,B))`;; let Ray_DEF = new_definition `! A B X. ray A B X <=> ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B)`;; let Ordered_DEF = new_definition `ordered A B C D <=> B IN open (A,C) /\ B IN open (A,D) /\ C IN open (A,D) /\ C IN open (B,D)`;; let InteriorAngle_DEF = new_definition `! A O B P. int_angle A O B P <=> ~Collinear A O B /\ ? a b. Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\ P NOTIN a /\ P NOTIN b /\ P,B same_side a /\ P,A same_side b`;; let InteriorTriangle_DEF = new_definition `! A B C P. int_triangle A B C P <=> P IN int_angle A B C /\ P IN int_angle B C A /\ P IN int_angle C A B`;; let Tetralateral_DEF = new_definition `Tetralateral A B C D <=> ~(A = B) /\ ~(A = C) /\ ~(A = D) /\ ~(B = C) /\ ~(B = D) /\ ~(C = D) /\ ~Collinear A B C /\ ~Collinear B C D /\ ~Collinear C D A /\ ~Collinear D A B`;; let Quadrilateral_DEF = new_definition `Quadrilateral A B C D <=> Tetralateral A B C D /\ open (A,B) INTER open (C,D) = {} /\ open (B,C) INTER open (D,A) = {} `;; let ConvexQuad_DEF = new_definition `ConvexQuadrilateral A B C D <=> Quadrilateral A B C D /\ A IN int_angle B C D /\ B IN int_angle C D A /\ C IN int_angle D A B /\ D IN int_angle A B C `;; let Segment_DEF = new_definition `seg A B = {A, B} UNION open (A,B)`;; let SEGMENT = new_definition `Segment s <=> ? A B. s = seg A B /\ ~(A = B)`;; let SegmentOrdering_DEF = new_definition `s <_seg t <=> Segment s /\ ? C D X. t = seg C D /\ X IN open (C,D) /\ s === seg C X`;; let Angle_DEF = new_definition ` angle A O B = ray O A UNION ray O B `;; let ANGLE = new_definition `Angle alpha <=> ? A O B. alpha = angle A O B /\ ~Collinear A O B`;; let AngleOrdering_DEF = new_definition `alpha <_ang beta <=> Angle alpha /\ ? A O B G. ~Collinear A O B /\ beta = angle A O B /\ G IN int_angle A O B /\ alpha === angle A O G`;; let RAY = new_definition `Ray r <=> ? O A. ~(O = A) /\ r = ray O A`;; let TriangleCong_DEF = new_definition `! A B C A' B' C' :point. (A, B, C) cong (A', B', C') <=> ~Collinear A B C /\ ~Collinear A' B' C' /\ seg A B === seg A' B' /\ seg A C === seg A' C' /\ seg B C === seg B' C' /\ angle A B C === angle A' B' C' /\ angle B C A === angle B' C' A' /\ angle C A B === angle C' A' B'`;; let SupplementaryAngles_DEF = new_definition `! alpha beta. alpha Suppl beta <=> ? A O B A'. ~Collinear A O B /\ O IN open (A,A') /\ alpha = angle A O B /\ beta = angle B O A'`;; let RightAngle_DEF = new_definition `! alpha. Right alpha <=> Angle alpha /\ ? beta. alpha Suppl beta /\ alpha === beta`;; let PlaneComplement_DEF = new_definition `! A:point alpha:point_set. complement alpha P <=> P NOTIN alpha`;; let CONVEX = new_definition `Convex alpha <=> ! A B. A IN alpha /\ B IN alpha ==> open (A,B) SUBSET alpha`;; (* ----------------------------------------------------------------- *) (* The axioms. *) (* ----------------------------------------------------------------- *) let I1 = new_axiom `! A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;; let I2 = new_axiom `! l. ? A B. Line l /\ A IN l /\ B IN l /\ ~(A = B)`;; let I3 = new_axiom `? A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear A B C`;; let B1 = new_axiom `! A B C. Between A B C ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Between C B A /\ Collinear A B C`;; let B2 = new_axiom `! A B. ~(A = B) ==> ? C. Between A B C`;; let B3 = new_axiom `! A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear A B C ==> (Between A B C \/ Between B C A \/ Between C A B) /\ ~(Between A B C /\ Between B C A) /\ ~(Between A B C /\ Between C A B) /\ ~(Between B C A /\ Between C A B)`;; let B4 = new_axiom `! l A B C. Line l /\ ~Collinear A B C /\ A NOTIN l /\ B NOTIN l /\ C NOTIN l /\ (? X. X IN l /\ Between A X C) ==> (? Y. Y IN l /\ Between A Y B) \/ (? Y. Y IN l /\ Between B Y C)`;; let C1 = new_axiom `! s O Z. Segment s /\ ~(O = Z) ==> ?! P. P IN ray O Z DELETE O /\ seg O P === s`;; let C2Reflexive = new_axiom `Segment s ==> s === s`;; let C2Symmetric = new_axiom `Segment s /\ Segment t /\ s === t ==> t === s`;; let C2Transitive = new_axiom `Segment s /\ Segment t /\ Segment u /\ s === t /\ t === u ==> s === u`;; let C3 = new_axiom `! A B C A' B' C'. B IN open (A,C) /\ B' IN open (A',C') /\ seg A B === seg A' B' /\ seg B C === seg B' C' ==> seg A C === seg A' C'`;; let C4 = new_axiom `! alpha O A l Y. Angle alpha /\ ~(O = A) /\ Line l /\ O IN l /\ A IN l /\ Y NOTIN l ==> ?! r. Ray r /\ ? B. ~(O = B) /\ r = ray O B /\ B NOTIN l /\ B,Y same_side l /\ angle A O B === alpha`;; let C5Reflexive = new_axiom `Angle alpha ==> alpha === alpha`;; let C5Symmetric = new_axiom `Angle alpha /\ Angle beta /\ alpha === beta ==> beta === alpha`;; let C5Transitive = new_axiom `Angle alpha /\ Angle beta /\ Angle gamma /\ alpha === beta /\ beta === gamma ==> alpha === gamma`;; let C6 = new_axiom `! A B C A' B' C'. ~Collinear A B C /\ ~Collinear A' B' C' /\ seg B A === seg B' A' /\ seg B C === seg B' C' /\ angle A B C === angle A' B' C' ==> angle B C A === angle B' C' A'`;; (* ----------------------------------------------------------------- *) (* Theorems. *) (* ----------------------------------------------------------------- *) let B1' = thm `; ! A B C. B IN open (A,C) ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ B IN open (C,A) /\ Collinear A B C by IN, Interval_DEF, B1`;; let B2' = thm `; ! A B. ~(A = B) ==> ? C. B IN open (A,C) by IN, Interval_DEF, B2`;; let B3' = thm `; ! A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear A B C ==> (B IN open (A,C) \/ C IN open (B,A) \/ A IN open (C,B)) /\ ~(B IN open (A,C) /\ C IN open (B,A)) /\ ~(B IN open (A,C) /\ A IN open (C,B)) /\ ~(C IN open (B,A) /\ A IN open (C,B)) by IN, Interval_DEF, B3`;; let B4' = thm `; ! l A B C. Line l /\ ~Collinear A B C /\ A NOTIN l /\ B NOTIN l /\ C NOTIN l /\ (? X. X IN l /\ X IN open (A,C)) ==> (? Y. Y IN l /\ Y IN open (A,B)) \/ (? Y. Y IN l /\ Y IN open (B,C)) by B4, IN, Interval_DEF`;; let B4'' = thm `; let l be point_set; let A B C be point; assume Line l [H0]; assume ~Collinear A B C /\ A NOTIN l /\ B NOTIN l /\ C NOTIN l [H1]; assume A,B same_side l /\ B,C same_side l [H2]; thus A,C same_side l by H0, H1, H2, B4', IN, SameSide_DEF`;; 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) by H1, H2, SING_SUBSET, SUBSET_ANTISYM, SUBSET, NOTIN, IN_SING`;; let DisjointOneNotOther_THM = thm `; let x be A; let l m be A->bool; assume l INTER m = {} [H1]; assume x IN m [H2]; thus x NOTIN l proof qed by H1, H2, NOTIN, IN_INTER, NOT_IN_EMPTY`;; let IntersectionSingletonOneNotOther_THM = thm `; let e x be A; let l m be A->bool; assume l INTER m = {x} [H1]; assume e IN l [H2]; assume ~(e = x) [H3]; thus e NOTIN m by H1, H2, H3, NOTIN, IN_INTER, IN_SING`;; let EquivIntersectionHelp_THM = thm `; let e x be A; let l m be A->bool; assume l INTER m = {x} [H1]; assume e IN m DELETE x [H2]; thus e NOTIN l by H1, H2, NOTIN, IN_DELETE, IntersectionSingletonOneNotOther_THM`;; let SubsetTensor_THM = thm `; let a b s be A->bool; assume a SUBSET b [H1]; thus a INTER s SUBSET b INTER s /\ s INTER a SUBSET s INTER b by H1, INTER_SUBSET, SUBSET_TRANS, SUBSET_INTER`;; let NonemptySubsetSing_THM = thm `; let a be A; let l be A->bool; assume ~(l = {}) [H1]; assume l SUBSET {a} [H2]; thus a IN l by H1, H2, MEMBER_NOT_EMPTY, SUBSET, IN_SING`;; let CollinearSymmetry_THM = thm `; let A B C be point; assume Collinear A B C [H1]; thus Collinear A C B /\ Collinear B A C /\ Collinear B C A /\ Collinear C A B /\ Collinear C B A by H1, Collinear_DEF`;; let OnePointImpliesAnother_THM = thm `; let P be point; thus ? Q:point. ~(Q = P) by I3`;; let ExistsPointOffLine_THM = thm `; let l be point_set; assume Line l [H1]; thus ? Q:point. Q NOTIN l by H1, I3, NOTIN, Collinear_DEF`;; let BetweenLinear_THM = thm `; ::solved at 849,716 let A B C be point; let m be point_set; assume Line m /\ A IN m /\ C IN m [H1]; assume B IN open (A,C) \/ C IN open (B,A) \/ A IN open (C,B) [H2]; thus B IN m by H1, H2, B1', Collinear_DEF, I1`;; let CollinearLinear_THM = thm `; let A B C be point; let m be point_set; assume Line m /\ A IN m /\ C IN m [H1]; assume Collinear A B C \/ Collinear B C A \/ Collinear C A B [H2]; assume ~(A = C) [H3]; thus B IN m by H1, H2, H3, Collinear_DEF, I1`;; let SameSideDisjointIntersection_THM = thm `; ! l A B. Line l ==> (A,B same_side l <=> open (A,B) INTER l = {}) by IN_INTER, SameSide_DEF, MEMBER_NOT_EMPTY`;; let NonCollinearImpliesDistinct_THM = thm `; ::solved at 1,050,293 let A B C be point; assume ~Collinear A B C [H1]; thus ~(A = B) /\ ~(A = C) /\ ~(B = C) by H1, OnePointImpliesAnother_THM, I1, Collinear_DEF`;; let OpenIntervalSubsetLine_THM = thm `; let A B be point; let l be point_set; assume Line l /\ A IN l /\ B IN l [H1]; thus open (A,B) SUBSET l by H1, BetweenLinear_THM, SUBSET`;; let SameSideDisjointLines_THM = thm `; let l m be point_set; let A B be point; assume Line m /\ A IN m /\ B IN m [m_line]; assume Line l [l_line]; assume m INTER l = {} [Disjoint]; thus A NOTIN l /\ B NOTIN l /\ A,B same_side l by m_line, l_line, Disjoint, IN_INTER, MEMBER_NOT_EMPTY, NOTIN, OpenIntervalSubsetLine_THM, SubsetTensor_THM, SUBSET_EMPTY, SameSideDisjointIntersection_THM`;; let Reverse4Order_THM = thm `; let A B C D be point; assume ordered A B C D [H1]; thus ordered D C B A by H1, Ordered_DEF, B1'`;; let OriginInRay_THM = thm `; let O Q be point; assume ~(Q = O) [H1]; thus O IN ray O Q by H1, B1', NOTIN, I1, Collinear_DEF, IN, Ray_DEF`;; let EndpointInRay_THM = thm `; let O Q be point; assume ~(Q = O) [H1]; thus Q IN ray O Q by H1, B1', NOTIN, I1, Collinear_DEF, IN, Ray_DEF`;; ------------------------------------------------------------------------------ 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
