Skip to content
Permalink
Browse files

updated quotes in Between hierarchy

  • Loading branch information...
carmenchui committed Jun 20, 2018
1 parent bbebb9c commit 754c8defdbb7e75765e30079e1f78ba4197bfeba
@@ -3,7 +3,7 @@

(cl-imports http://colore.oor.net/between/betweenness.clif)

(cl-comment "Axiom C")
(cl-comment 'Axiom C')

(forall (a b1 b2 c d)
(if (and (between a c b1)
@@ -12,7 +12,7 @@
(and (between b1 b b2)
(between a d b)))))

(cl-comment "Axiom L1")
(cl-comment 'Axiom L1')

(forall (a b)
(if (between a b a)
@@ -3,7 +3,7 @@

(cl-imports http://colore.oor.net/between/coppel_pasch.clif)

(cl-comment "Axiom L2")
(cl-comment 'Axiom L2')
(forall (a b c d)
(if (and (between a b c)
(between b c d)
@@ -3,7 +3,7 @@

(cl-imports http://colore.oor.net/between/convex_coppel.clif)

(cl-comment "Axiom P")
(cl-comment 'Axiom P')

(forall (a b1 b2 c1 c2)
(if (and (between a c1 b1)
@@ -1,49 +1,49 @@

(cl-text http://colore.oor.net/between/inner_pasch.clif

(cl-comment "A1")
(cl-comment 'A1')
(forall (a b c)
(if (between a b c)
(between c b a)))

(cl-comment "A2")
(cl-comment 'A2')
(forall (a b c)
(if (between a b c)
(not (between a c b))))

(cl-comment "A3")
(cl-comment 'A3')
(forall (a b c d)
(if (and (between a b c)
(between a b d))
(between c b d)))

(cl-comment "A4")
(cl-comment 'A4')
(forall (a b c d)
(if (and (between c a b)
(between a b d))
(between c b d)))

(cl-comment "A5")
(cl-comment 'A5')
(forall (a b c d)
(if (and (between a b c)
(between a b d)
(not (= c d)))
(or (between b c d)
(between b d c))))

(cl-comment "A6")
(cl-comment 'A6')
(forall (a b)
(if (not (= a b))
(exists (c)
(between a b c))))

(cl-comment "A7")
(cl-comment 'A7')
(forall (a b)
(if (not (= a b))
(exists (c)
(between a c b ))))

(cl-comment "IP")
(cl-comment 'IP')
(forall (a b c d e)
(if (and (not (L a b c))
(between a b d)
@@ -1,39 +1,39 @@
(cl-text http://colore.oor.net/between/lewand.clif

(cl-comment "A2.2")
(cl-comment 'A2.2')
(forall (a b c)
(if (between a b c)
(between c b a)))

(cl-comment "A2.6")
(cl-comment 'A2.6')
(forall (x y a b)
(if (and (between x a b)
(between a y b))
(between x a y)))

(cl-comment "A2.34")
(cl-comment 'A2.34')
(forall (a b c)
(or (between a b c)
(between b c a)
(between c a b)))

(cl-comment "A2.35")
(cl-comment 'A2.35')
(forall (a b)
(if (between a b a)
(= a b)))

(cl-comment "A2.38")
(cl-comment 'A2.38')
(exists (p1 p2)
(not (= p1 p2)))

(cl-comment "A2.40")
(cl-comment 'A2.40')
(forall (a c)
(if (not (= a c))
(exists (b)
(and (between a b c)
(not (= c b))))))

(cl-comment "A2.39")
(cl-comment 'A2.39')
(forall (a b)
(if (not (= a b))
(exists (c)
@@ -1,49 +1,49 @@

(cl-text http://colore.oor.net/between/outer_pasch.clif

(cl-comment "A1")
(cl-comment 'A1')
(forall (a b c)
(if (between a b c)
(between c b a)))

(cl-comment "A2")
(cl-comment 'A2')
(forall (a b c)
(if (between a b c)
(not (between a c b))))

(cl-comment "A3")
(cl-comment 'A3')
(forall (a b c d)
(if (and (between a b c)
(between a b d))
(between c b d)))

(cl-comment "A4")
(cl-comment 'A4')
(forall (a b c d)
(if (and (between c a b)
(between a b d))
(between c b d)))

(cl-comment "A5")
(cl-comment 'A5')
(forall (a b c d)
(if (and (between a b c)
(between a b d)
(not (= c d)))
(or (between b c d)
(between b d c))))

(cl-comment "A6")
(cl-comment 'A6')
(forall (a b)
(if (not (= a b))
(exists (c)
(between a b c))))

(cl-comment "A7")
(cl-comment 'A7')
(forall (a b)
(if (not (= a b))
(exists (c)
(between a c b ))))

(cl-comment "OP")
(cl-comment 'OP')
(forall (a b c d e)
(if (and (not (L a b c))
(between a b d)
@@ -20,7 +20,7 @@
(between z x y)
(between y z x))))

(cl-comment "Although this relation is not explicit in Fishburn, it captures the notion of two elements appearing in the same triple.")
(cl-comment 'Although this relation is not explicit in Fishburn, it captures the notion of two elements appearing in the same triple.')
(forall (x y)
(iff (same_triple x y)
(exists (z)
@@ -1,19 +1,19 @@
(cl-text http://colore.oor.net/between/tarski_between.clif

(cl-comment "Givant:Ax6, Tarski59:A1")
(cl-comment 'Givant:Ax6, Tarski59:A1')
(forall (x y)
(if (between x y x)
(= x y)))

(cl-comment "Givant:Ax7.2")
(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(2).1, Tarski51:A12")
(cl-comment 'Givant:Ax9(2).1, Tarski51:A12')
(forall (x a b c)
(exists (y)
(or (and (or (between x y z)
@@ -29,7 +29,7 @@
(between c x y))
(between a y b)))))

(cl-comment "Givant:Ax10, Tarski59:A8")
(cl-comment 'Givant:Ax10, Tarski59:A8')
(forall (a b c d t)
(if (and (between a d t)
(between b d c)
@@ -39,36 +39,36 @@
(between a c y)
(between x t y)))))

(cl-comment "Givant:Ax12")
(cl-comment 'Givant:Ax12')
(forall (a b)
(between a b b))

(cl-comment "Givant:Ax14")
(cl-comment 'Givant:Ax14')
(forall (a b c)
(if (between a b c)
(between c b a)))

(cl-comment "Givant:Ax15, Tarski59:A2")
(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")
(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")
(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")
(cl-comment 'Givant:Ax18, Tarski59:A3')
(forall (a b c d)
(if (and (between a b c)
(between a b d)
@@ -1,25 +1,25 @@
(cl-text http://colore.oor.net/between/tarski_linear.clif

(cl-comment "Givant:Ax6, Tarski59:A1")
(cl-comment 'Givant:Ax6, Tarski59:A1')
(forall (x y)
(if (between x y x)
(= x y)))

(cl-comment "Givant:Ax7.2")
(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")
(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")
(cl-comment 'Givant:Ax10, Tarski59:A8')
(forall (a b c d t)
(if (and (between a d t)
(between b d c)
@@ -29,36 +29,36 @@
(between a c y)
(between x t y)))))

(cl-comment "Givant:Ax12")
(cl-comment 'Givant:Ax12')
(forall (a b)
(between a b b))

(cl-comment "Givant:Ax14")
(cl-comment 'Givant:Ax14')
(forall (a b c)
(if (between a b c)
(between c b a)))

(cl-comment "Givant:Ax15, Tarski59:A2")
(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")
(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")
(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")
(cl-comment 'Givant:Ax18, Tarski59:A3')
(forall (a b c d)
(if (and (between a b c)
(between a b d)
@@ -2,7 +2,7 @@

(cl-imports http://colore.oor.net/between/infinite_bet.clif)

(cl-comment "(cl-imports http://colore.oor.net/between/pasch.clif)")
(cl-comment '(cl-imports http://colore.oor.net/between/pasch.clif)')

(exists (p1 p2)
(not (= p1 p2)))

0 comments on commit 754c8de

Please sign in to comment.
You can’t perform that action at this time.