-
Notifications
You must be signed in to change notification settings - Fork 35
/
tarski_linear.clif
70 lines (58 loc) · 1.35 KB
/
tarski_linear.clif
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
(cl-text http://colore.oor.net/between/tarski_linear.clif
(cl-comment 'Givant:Ax6, Tarski59:A1')
(forall (x y)
(if (between x y x)
(= x y)))
(cl-comment 'Givant:Ax7.2')
(forall (a b c p q)
(if (and (between a p c)
(between q c b))
(exists (x)
(and (between x p b)
(between a x q)))))
(cl-comment 'Givant:Ax9.1, Tarski51:A12')
(forall ( a b c)
(or (between a b c)
(between b c a)
(between c a b)))
(cl-comment 'Givant:Ax10, Tarski59:A8')
(forall (a b c d t)
(if (and (between a d t)
(between b d c)
(not (= a d)))
(exists (x y)
(and (between a b x)
(between a c y)
(between x t y)))))
(cl-comment 'Givant:Ax12')
(forall (a b)
(between a b b))
(cl-comment 'Givant:Ax14')
(forall (a b c)
(if (between a b c)
(between c b a)))
(cl-comment 'Givant:Ax15, Tarski59:A2')
(forall (a b c d)
(if (and (between a b d)
(between b c d))
(between a b c)))
(cl-comment 'Givant:Ax16')
(forall (a b c d)
(if (and (between a b c)
(between b c d)
(not (= b c)))
(between a b d)))
(cl-comment 'Givant:Ax17')
(forall (a b c d)
(if (and (between a b d)
(between a c d))
(or (between a b c)
(between a c b))))
(cl-comment 'Givant:Ax18, Tarski59:A3')
(forall (a b c d)
(if (and (between a b c)
(between a b d)
(not (= a b)))
(or (between a c d)
(between a d c))))
)