% problem-set/geometry/tarski/axioms.ver3 % created : 07/20/89 % revised : 08/07/89 % description : % % These axioms are an adaptation from Quaife, "Automated Development of % Tarski's Geometry" [Journal of Automated Reasoning 5 (1989) pp.97-118]. % representation : % % declare_predicates(3,[B,C]). % declare_predicates(2,[=,EQ]). % declare_function(6,cont). % declare_functions(5,[ip,euc1,euc2]). % declare_functions(4,[ext,ins]). % declare_functions(2,[dist,R]). % declare_constants([C1,C2,C3,a,b,c,d,e]). % declare_variables([u,u1,v,v1,w,w1,x,x1,y,y1,z,z1]). % % Important Note: the Axiom Numbers are different between the two versions!! % % Note that L from version 1 has been replaced entirely, L(x,y,z,w) being % replaced by (dist(x,y) = dist(z,w)); C1, C2, and C3 are p, p', and p'' % from Quaife's paper; and that skolem functions have been named for purposes % of consistency and readability. Also, the weak form of the continuity axiom % is used, just as in version 1. % % B(x,y,z) : y is between x and z. % C(x,y,z) : x, y, and z are collinear. % (x = y) : x and y are distances that are equal % EQ(x,y) : x and y are points that are equal % cont : Skolem function arising from the Weakened form of the Elementary % Continuity axiom (A13') % ip : Skolem function arising from Pasch's axiom (A7) % euc1 : Skolem function arising from Euclid's axiom (A8) % euc2 : Skolem function arising from Euclid's axiom (A8) % ext : Skolem function arising from the Segment Construction axiom (A10) % ins : insertion function (I1) % dist : function naming the distance from x to y % R : reflection function (R1) % C1, C2, C3 : Skolem constants arising from the Lower Dimension axiom (A11) % A1 : Reflexivity axiom for equidistance (dist(u,v) = dist(v,u)). % A2 : Transitivity axiom for equidistance (dist(u,v) != dist(w,x)) | (dist(u,v) != dist(y,z)) | (dist(w,x) = dist(y,z)). % A3 : Identity axiom for equidistance (dist(u,v) != dist(w,w)) | EQ(u,v). % A4 : Segment Construction Axiom B(u,v,ext(u,v,w,x)). (dist(v,ext(u,v,w,x)) = dist(w,x)). % A5 : Outer Five-Segment Axiom (dist(u,v) != dist(u1,v1)) | (dist(v,w) != dist(v1,w1)) | (dist(u,x) != dist(u1,x1)) | (dist(v,x) != dist(v1,x1)) | (dist(w,x) = dist(w1,x1)) | -B(u,v,w) | -B(u1,v1,w1) | EQ(u,v). % A6 : Identity axiom for betweenness -B(u,v,u) | EQ(u,v). % A7 : Inner Pasch Axiom B(v,ip(u,v,w,x,y),y) | -B(u,v,w) | -B(y,x,w). B(x,ip(u,v,w,x,y),u) | -B(u,v,w) | -B(y,x,w). % A8 : Lower Dimension Axiom -B(C1,C2,C3). -B(C2,C3,C1). -B(C3,C1,C2). % A9 : Upper Dimension Axiom % (dist(u,x) != dist(u,y)) | (dist(v,x) != dist(v,y)) | % (dist(w,x) != dist(w,y)) | B(u,v,w) | B(v,w,u) | B(w,u,v) | EQ(x,y). % A10 : Euclid's Axiom % B(u,v,euc1(u,v,w,x,y)) | -B(u,w,y) | -B(v,w,x) | EQ(u,w). % B(u,x,euc2(u,v,w,x,y)) | -B(u,w,y) | -B(v,w,x) | EQ(u,w). % B(euc1(u,v,w,x,y),y,euc2(u,v,w,x,y)) | -B(u,w,y) | -B(v,w,x) | EQ(u,w). % A11 : Elementary Continuity Axiom (Weak Form) % (dist(u,v) != dist(u,v1)) | (dist(u,x) != dist(u,x1)) | % B(v1,cont(u,v,v1,w,x,x1),x1) | -B(u,v,x) | -B(v,w,x). % (dist(u,v) != dist(u,v1)) | (dist(u,x) != dist(u,x1)) | % (dist(u,w) = dist(u,cont(u,v,v1,w,x,x1))) | -B(u,v,x) | -B(v,w,x). % Reflexivity of Equality (x = x). EQ(x,x). % R1 : Definition of reflection % EQ(ext(u,v,u,v),R(u,v)). % I1 : Definition of insertion % EQ(ext(ext(w1,u1,C1,C2),u1,u,v),ins(u1,w1,u,v)). % C1 : Definition of Collinearity % -B(u,v,w) | C(u,v,w). % -B(v,w,u) | C(u,v,w). % -B(w,u,v) | C(u,v,w). % -C(u,v,w) | B(u,v,w) | B(v,w,u) | B(w,u,v). % B12 : Connectivity axiom for betweenness -B(u,v,w) | -B(u,v,x) | B(u,w,x) | B(u,x,w) | EQ(u,v).