I'm glad I can be useful.
This is the code
g (`!a b c. ~(a=b:tarski) /\ ~ (a=c:tarski) /\ ~ (b=c:tarski) /\ COLL
(a,b,c) ==> (BB(a,b,c)\/BB (b,c,a)\/BB (c,a,b)) /\
~(BB(a,b,c) /\ BB(b,c,a)) /\
~(BB(a,b,c)/\BB(c,a,b)) /\
~(BB(b,c,a)/\BB(c,a,b))`);;
e (REPEAT STRIP_TAC);;
e (ASM_MESON_TAC [COLL]);;
e (BB_ASM_MESON_TAC [BB_ID]);;
e (BB_ASM_MESON_TAC [BB_ID]);;
e (BB_ASM_MESON_TAC [BB_ID]);;
let B3=top_thm();;
Following Narboux's example BB_ASM_MESON_TAC is a tactic summarizing easy
betweenness properties (as the identity axiom for betweenness and some
transitivity properties, from which follow the conclusion).
I have a copy of Tarski's book, but unfortunately I don't speak german
either. I'll try to interpretate this part and let you know.
2012/7/8 Bill Richter <[email protected]>
> Thanks, Lorenzo! I'd be grateful if you could teach me some Tarski
> geometry, apart from any proof assistant formalization. The last time
> I looked, it seemed that Julien Narboux hadn't quite proved the
> existence of midpoints, nor Hilbert's full Pasch axiom
>
> 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)`;;
>
> I'm embarrassed that I can't prove these things myself, and I'm even
> starting to wonder if Tarski actually proved these things. There is
> no paper written in English proving Hilbert's axioms from Tarski's.
> Your Tarski book, which I don't have, is written in German, by
> Schwabhäuser I believe. Can you read it and post some proofs?
>
> --
> 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
