% problem-set/geometry/tarski/t9.ver1.in % created : 07/16/86 % revised : 08/08/89 % description : % Theorem T9: For all points x, y, z, and w, if y and w are between x and % z, then either y is between x and w or w is between x and y. % representation : % % declare_predicates(4,[L]). % declare_predicates(3,[B,C]). % declare_predicates(2,[EQ]). % declare_functions(6,[cont]). % declare_functions(5,[op,euc1,euc2]). % declare_functions(4,[ext]). % declare_constants([C1,C2,C3,a,b,c,d,e]). % declare_variables([u,v,w,x,y,z,v1,v2,v3,v4,v5,x1,y1,z1]). % % Note that skolem functions have been renamed to agree with the second % axiom set's names, for purposed of consistency and readability. Also, % the weakened form of the continuity axiom, axiom A13', is used. % % B(x,y,z) : y is between x and z. % L(x1,y1,x2,y2) : the distance from x1 to y1 equals that from x2 to y2. % C1, C2, C3 : Skolem constants arising from the Lower Dimension Axiom (A11) % op : Skolem function arising from Outer Pasch 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) % cont : Skolem function arising from the Weakened form of the Elementary % Continuity Axiom (A13') lex([a, b, c, d, e, C1, C2, C3, ext(x,y,z,w), op(x,y,z,u,v), B(x,y,z), C(x,y,z), L(x,y,v,w)]). set(hyper_res). set(ur_res). set(dynamic_demod). set(order_eq). set(unit_deletion). assign(max_mem,3000). assign(max_seconds,1800). set_skolem([ext(x,y,z,w), op(u,v,w,x,y)]). % set_skolem([euc1(u,v,w,x,y), euc2(u,v,w,x,y), cont(u,v,w,x,y,z)]). set(delete_identical_nested_skolem). assign(max_weight,50). % with atom demodulators; list(axioms). % A8 : 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). % A13 : Continuity Axiom (Weak Form) % -L(v,x,v,x1) | -L(v,z,v,z1) | -B(v,x,z) | -B(x,y,z) | L(v,y,v,cont(x,y,z,x1,z1,v)). % -L(v,x,v,x1) | -L(v,z,v,z1) | -B(v,x,z) | -B(x,y,z) | B(x1,cont(x,y,z,x1,z1,v),z1). % Equality axioms EQ(x,x). -EQ(x,y) | EQ(y,x). -EQ(x,y) | -EQ(y,z) | EQ(x,z). % Equality Substitution Axioms -B(x,w,z) | B(y,w,z) | -EQ(x,y). -B(w,x,z) | B(w,y,z) | -EQ(x,y). -B(w,z,x) | B(w,z,y) | -EQ(x,y). % -C(x,w,z) | C(y,w,z) | -EQ(x,y). % -C(w,x,z) | C(w,y,z) | -EQ(x,y). % -C(w,z,x) | C(w,z,y) | -EQ(x,y). -L(x,v,w,z) | L(y,v,w,z) | -EQ(x,y). -L(v,x,w,z) | L(v,y,w,z) | -EQ(x,y). -L(v,w,x,z) | L(v,w,y,z) | -EQ(x,y). -L(v,w,z,x) | L(v,w,y,z) | -EQ(x,y). EQ(op(x,v1,v2,v3,v4),op(y,v1,v2,v3,v4)) | -EQ(x,y). EQ(op(v1,x,v2,v3,v4),op(v1,y,v2,v3,v4)) | -EQ(x,y). EQ(op(v1,v2,x,v3,v4),op(v1,v2,y,v3,v4)) | -EQ(x,y). EQ(op(v1,v2,v3,x,v4),op(v1,v2,v3,y,v4)) | -EQ(x,y). EQ(op(v1,v2,v3,v4,x),op(v1,v2,v3,v4,y)) | -EQ(x,y). % EQ(euc1(x,v1,v2,v3,v4),euc1(y,v1,v2,v3,v4)) | -EQ(x,y). % EQ(euc1(v1,x,v2,v3,v4),euc1(v1,y,v2,v3,v4)) | -EQ(x,y). % EQ(euc1(v1,v2,x,v3,v4),euc1(v1,v2,y,v3,v4)) | -EQ(x,y). % EQ(euc1(v1,v2,v3,x,v4),euc1(v1,v2,v3,y,v4)) | -EQ(x,y). % EQ(euc1(v1,v2,v3,v4,x),euc1(v1,v2,v3,v4,y)) | -EQ(x,y). % EQ(euc2(x,v1,v2,v3,v4),euc2(y,v1,v2,v3,v4)) | -EQ(x,y). % EQ(euc2(v1,x,v2,v3,v4),euc2(v1,y,v2,v3,v4)) | -EQ(x,y). % EQ(euc2(v1,v2,x,v3,v4),euc2(v1,v2,y,v3,v4)) | -EQ(x,y). % EQ(euc2(v1,v2,v3,x,v4),euc2(v1,v2,v3,y,v4)) | -EQ(x,y). % EQ(euc2(v1,v2,v3,v4,x),euc2(v1,v2,v3,v4,y)) | -EQ(x,y). EQ(ext(x,v1,v2,v3),ext(y,v1,v2,v3)) | -EQ(x,y). EQ(ext(v1,x,v2,v3),ext(v1,y,v2,v3)) | -EQ(x,y). EQ(ext(v1,v2,x,v3),ext(v1,v2,y,v3)) | -EQ(x,y). EQ(ext(v1,v2,v3,x),ext(v1,v2,v3,y)) | -EQ(x,y). % EQ(cont(x,v1,v2,v3,v4,v5),cont(y,v1,v2,v3,v4,v5)) | -EQ(x,y). % EQ(cont(v1,x,v2,v3,v4,v5),cont(v1,y,v2,v3,v4,v5)) | -EQ(x,y). % EQ(cont(v1,v2,x,v3,v4,v5),cont(v1,v2,y,v3,v4,v5)) | -EQ(x,y). % EQ(cont(v1,v2,v3,x,v4,v5),cont(v1,v2,v3,y,v4,v5)) | -EQ(x,y). % EQ(cont(v1,v2,v3,v4,x,v5),cont(v1,v2,v3,v4,y,v5)) | -EQ(x,y). % EQ(cont(v1,v2,v3,v4,v5,x),cont(v1,v2,v3,v4,v5,y)) | -EQ(x,y). end_of_list. list(sos). % A1 : Identity axiom for betweenness -B(x,y,x) | EQ(x,y). % A2 : Transitivity axiom for betweenness -B(x,y,v) | -B(y,z,v) | B(x,y,z). % A3 : Connectivity axiom for betweenness -B(x,y,z) | -B(x,y,v) | B(x,z,v) | B(x,v,z) | EQ(x,y). % A4 : Reflexivity axiom for equidistance L(x,y,y,x). % A5 : Identity axiom for equidistance -L(x,y,z,z) | EQ(x,y). % A6 : Transitivity axiom for equidistance -L(x,y,z,v) | -L(x,y,v2,w) | L(z,v,v2,w). % A7 : Outer Pasch Axiom B(x,op(w,x,y,z,v),y) | -B(x,w,v) | -B(y,v,z). B(z,w,op(w,x,y,z,v)) | -B(x,w,v) | -B(y,v,z). % A9 : Five Segment Axiom -L(x,y,x1,y1) | -L(y,z,y1,z1) | -L(x,v,x1,v1) | -L(y,v,y1,v1) | L(z,v,z1,v1) | -B(x,y,z) | -B(x1,y1,z1) | EQ(x,y). % A10 : Segment Construction Axiom B(x,y,ext(x,y,w,v)). L(y,ext(x,y,w,v),w,v). % A11 : Lower Dimension Axiom -B(C1,C2,C3). -B(C2,C3,C1). -B(C3,C1,C2). % A12 : Upper Dimension Axiom -L(x,w,x,v) | -L(y,w,y,v) | -L(z,w,z,v) | B(x,y,z) | B(y,z,x) | B(z,x,y) | EQ(w,v). % Definition of Collinearity % -C(x,y,z) | B(x,y,z) | B(y,x,z) | B(x,z,y). % -B(x,y,z) | C(x,y,z). % -B(y,x,z) | C(x,y,z). % -B(x,z,y) | C(x,y,z). % T1 : -B(x,y,z) | B(z,y,x). % T2 : B(x,x,y). % T3 : B(x,y,y). % T6 : -B(x,y,z) | -B(x,z,y) | EQ(x,y) | EQ(y,z) | EQ(x,z). -B(x,y,z) | -B(y,x,z) | EQ(x,y) | EQ(y,z) | EQ(x,z). % T7 : -B(w,y,z) | -B(x,y,z) | B(x,w,y) | B(w,x,y) | EQ(y,z). % T8 : -B(x,y,z) | -B(x,w,z) | -B(y,v,w) | B(x,v,z). % T10 : % -C(x,y,z) | C(x,z,y). % -C(x,y,z) | C(y,x,z). % -C(x,y,z) | C(y,z,x). % -C(x,y,z) | C(z,x,y). % -C(x,y,z) | C(z,y,x). % T11 : % -C(C1,C2,C3). % denial of the theorem: B(a,c,e). B(a,d,e). -B(a,c,d). -B(a,d,c). end_of_list. list(demodulators). EQ(ext(x,y,z,z),y). % literal demodulators: (B(x,y,x) = EQ(x,y)). (L(x,y,z,z) = EQ(x,y)). (L(x,y,y,x) = $T). % (B(x,y,ext(x,y,w,v)) = $T). % (L(y,ext(x,y,w,v),w,v) = $T). (B(C1,C2,C3) = $F). (B(C2,C3,C1) = $F). (B(C3,C1,C2) = $F). (B(x,x,y) = $T). (B(x,y,y) = $T). % (C(C1,C2,C3) = $F). % lex-dependant (EQ(x,y) = EQ(y,x)). (B(x,y,z) = B(z,y,x)). % (C(x,y,z) = C(x,z,y)). % (C(x,y,z) = C(y,x,z)). % (C(x,y,z) = C(y,z,x)). % (C(x,y,z) = C(z,x,y)). % (C(x,y,z) = C(z,y,x)). (L(x,y,z,w) = L(z,w,x,y)). (L(x,y,z,w) = L(x,y,w,z)). (L(x,y,z,w) = L(y,x,z,w)). end_of_list. weight_list(pick_and_purge). % to purge (almost all) non-ground clauses weight(x,20). weight(C1,1). weight(C2,1). weight(C3,1). weight(a,0). weight(b,0). weight(c,0). weight(d,0). weight(e,0). weight(ext(1,1,1,1),5). weight(op(2,2,2,2,2),5). % weight(euc1(2,2,2,2,2),5). % weight(euc2(2,2,2,2,2),5). % weight(cont(2,2,2,2,2,2),5). end_of_list.