Freek, that's a great tip, timeout := 10;;, and it solved the B4'
problem I posted earlier, with the working code now in
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar
let B4' = thm `;
∀ l A B C. Line l ∧ ¬Collinear A B C ∧
¬(A ∈ l) ∧ ¬(B ∈ l) ∧ ¬(C ∈ l) ∧
(∃ X. X ∈ l ∧ X ∈ open (A,C)) ⇒
(∃ Y. Y ∈ l ∧ Y ∈ open (A,B)) ∨ (∃ Y. Y ∈ l ∧ Y ∈ open (B,C))
by B4, IN, Interval_DEF`;;
This doesn't look like a big deal, as I'm merely rewriting axiom B4
using open intervals instead of Between, but miz3 reports
..solved at 126459
That's my first 6-digit `solved at' number! Without setting timeout
to 5, miz3 easily proved the related result with `solved at 8751':
let B3' = thm `;
∀ A B C. ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Collinear A B C
⇒ (B ∈ open (A,C) ∨ C ∈ open (B,A) ∨ A ∈ open (C,B)) ∧
¬(B ∈ open (A,C) ∧ C ∈ open (B,A)) ∧
¬(B ∈ open (A,C) ∧ A ∈ open (C,B)) ∧
¬(C ∈ open (B,A) ∧ A ∈ open (C,B))
by IN, Interval_DEF, B3`;;
Without your timeout stunt, I had to needed a proof twice as long
let B4prime_THM = thm `;
let l be point_set;
let A B C be point;
assume Line l ∧ ¬Collinear A B C ∧
¬(A ∈ l) ∧ ¬(B ∈ l) ∧ ¬(C ∈ l) ∧
(∃ X. X ∈ l ∧ X ∈ open (A,C)) [H1];
thus (∃ Y. Y ∈ l ∧ Y ∈ open (A,B)) ∨ (∃ Y. Y ∈ l ∧ Y ∈ open (B,C))
proof
Line l ∧ ¬Collinear A B C ∧
¬(A ∈ l) ∧ ¬(B ∈ l) ∧ ¬(C ∈ l) ∧
(∃ X. X ∈ l ∧ Between A X C) by H1, IN, Interval_DEF;
(∃ Y. Y ∈ l ∧ Between A Y B) ∨ (∃ Y. Y ∈ l ∧ Between B Y C) by -, B4;
qed by -, IN, Interval_DEF`;;
That's in the version of my code with fancy math characters, which I
use Emacs to turn back into HOL Light terms. I realized I was getting
too much of a good thing when I saw, in one of my proofs,
{x} ⊂ p by H1, S∈G_⊂;
I realized that HOL Light was seeing
{x} SUBSET p by H1, SING_SUBSET;
because I was transforming the sets.ml thm names with Emacs code like
(goto-char (point-min))
(while (search-forward "∈" nil t)
(replace-match "IN" nil t))
so I changed the Emacs code to
(goto-char (point-min))
(while (search-forward " ∈ " nil t)
(replace-match " IN " nil t))
--
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
