Skip to content
Permalink
Browse files

updated comments in tarski_geometry with single quotes

  • Loading branch information...
carmenchui committed Jun 20, 2018
1 parent 18b3ba2 commit 619e55e05a7a9d416174d6b9dc06c65a676df9ef
@@ -13,20 +13,20 @@
(between x u z)
(= x y))))

(cl-comment "Identity of Betweenness")
(cl-comment 'Identity of Betweenness')
(forall (x y z)
(if (between x y x)
(= x y)))

(cl-comment "Axiom of Pasch")
(cl-comment 'Axiom of Pasch')
(forall (x y z u v)
(if (and (between x u z)
(between y v z))
(exists (a)
(and (between u a y)
(between v a x)))))

(cl-comment "There exist three noncollinear points")
(cl-comment 'There exist three noncollinear points')
(exists (x y z)
(and (not (between x y z))
(not (between y z x))
@@ -3,8 +3,8 @@

(cl-imports http://colore.oor.net/tarski_geometry/weak_tarski.clif)

(cl-comment "A segment which joins two points, one inside and one outside
the given circle, always intersects the circle.")
(cl-comment 'A segment which joins two points, one inside and one outside
the given circle, always intersects the circle.')

(forall (x y z x1 z1 u)
(exists (y1)
@@ -3,22 +3,22 @@

(cl-imports http://colore.oor.net/tarski_geometry/between_tarski.clif)

(cl-comment "Reflexivity of Congruence")
(cl-comment 'Reflexivity of Congruence')
(forall (x y)
(congruent x y y x))

(cl-comment "Identity of Congruence")
(cl-comment 'Identity of Congruence')
(forall (x y z)
(if (congruent x y z z)
(= x y)))

(cl-comment "Transitivity of Congruence")
(cl-comment 'Transitivity of Congruence')
(forall (x y z u v w)
(if (and (congruent x y z u)
(congruent x y v w))
(congruent z u v w)))

(cl-comment "Three points equidistant from two distinct points form a line.")
(cl-comment 'Three points equidistant from two distinct points form a line.')
(forall (x y z u v)
(if (and (congruent x u x v)
(congruent y u y v)
@@ -28,7 +28,7 @@
(between y z x)
(between z x y))))

(cl-comment "Five Segment Axiom")
(cl-comment 'Five Segment Axiom')
(forall (x y z u x1 y1 z1 u1)
(if (and (between x y z)
(not (= x y))
@@ -39,7 +39,7 @@
(congruent y u y1 u1))
(congruent z u z1 u1)))

(cl-comment "Given any two line segments, the second can be 'extended' by a line segment congruent to the first.")
(cl-comment 'Given any two line segments, the second can be 'extended' by a line segment congruent to the first.')
(forall (x y z w)
(exists (a)
(and (between w x a)
@@ -3,7 +3,7 @@

(cl-imports http://colore.oor.net/tarski_geometry/between_tarski.clif)

(cl-comment "Axiom of Continuity")
(cl-comment 'Axiom of Continuity')
(forall (p q)
(if (exists (a)
(forall (x y)
@@ -3,7 +3,7 @@

(cl-imports http://colore.oor.net/tarski_geometry/neutral_tarski.clif)

(cl-comment "It is not the case that given any angle and any point v in its interior, there exists a line segment including v, with an endpoint on each side of the angle.")
(cl-comment 'It is not the case that given any angle and any point v in its interior, there exists a line segment including v, with an endpoint on each side of the angle.')
(not (forall (x y z u v)
(if (and (between x u v)
(between y u z)
@@ -3,7 +3,7 @@

(cl-imports http://colore.oor.net/tarski_geometry/congruent_tarski.clif)

(cl-comment "Given any angle and any point v in its interior, there exists a line segment including v, with an endpoint on each side of the angle.")
(cl-comment 'Given any angle and any point v in its interior, there exists a line segment including v, with an endpoint on each side of the angle.')
(forall (x y z u v)
(if (and (between x u v)
(between y u z)

0 comments on commit 619e55e

Please sign in to comment.
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.