% problem-set/geometry/tarski/t11.ver2.in % created : 07/25/89 % revised : 07/26/89 % description : % % Theorem T11: The three points C1, C2, and C3 specified are NOT collinear. % representation : % % declare_predicates(3,[B,C]). % declare_predicates(2,[D,=]). % 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 D(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. % D(x,y) : x is the same length as y % 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) set(hyper_res). set(order_eq). set(unit_deletion). assign(max_weight,40). assign(max_seconds,1800). assign(max_mem,1500). set_skolem([ext(x,y,z,w), ip(u,v,w,x,y)]). set(delete_identical_nested_skolem). list(axioms). % A9 : Upper Dimension Axiom % -D(dist(u,x),dist(u,y)) | -D(dist(v,x),dist(v,y)) | % -D(dist(w,x),dist(w,y)) | B(u,v,w) | B(v,w,u) | B(w,u,v) | (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) % -D(dist(u,v),dist(u,v1)) | -D(dist(u,x),dist(u,x1)) | % B(v1,cont(u,v,v1,w,x,x1),x1) | -B(u,v,x) | -B(v,w,x). % -D(dist(u,v),dist(u,v1)) | -D(dist(u,x),dist(u,x1)) | % D(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). % R1 : Definition of reflection % (ext(u,v,u,v) = R(u,v)). % I1 : Definition of insertion % (ext(ext(w1,u1,C1,C2),u1,u,v) = ins(u1,w1,u,v)). end_of_list. list(sos). % denial of the theorem: C(C1,C2,C3). % A1 : Reflexivity axiom for equidistance D(dist(u,v),dist(v,u)). % A2 : Transitivity axiom for equidistance -D(dist(u,v),dist(w,x)) | -D(dist(u,v),dist(y,z)) | D(dist(w,x),dist(y,z)). % A3 : Identity axiom for equidistance -D(dist(u,v),dist(w,w)) | (u = v). % A4 : Segment Construction Axiom B(u,v,ext(u,v,w,x)). D(dist(v,ext(u,v,w,x)),dist(w,x)). % A5 : Outer Five-Segment Axiom -D(dist(u,v),dist(u1,v1)) | -D(dist(v,w),dist(v1,w1)) | -D(dist(u,x),dist(u1,x1)) | -D(dist(v,x),dist(v1,x1)) | D(dist(w,x),dist(w1,x1)) | -B(u,v,w) | -B(u1,v1,w1) | (u = v). % A6 : Identity axiom for betweenness -B(u,v,u) | (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). % B12 : Connectivity axiom for betweenness -B(u,v,w) | -B(u,v,x) | B(u,w,x) | B(u,x,w) | (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). end_of_list. list(demodulators). (ext(u,v,u,v) = R(u,v)). (ext(ext(w1,u1,C1,C2),u1,u,v) = ins(u1,w1,u,v)). end_of_list. weight_list(pick_and_purge). % to purge (almost all) non-ground clauses weight(x,20). weight(C1,0). weight(C2,0). weight(C3,0). end_of_list.