name(c82_). :- dynamic p/2,l/2,i/2. %domain elements dom(a1). dom(b1). dom(c1). dom(a2). dom(b2). dom(c2). dom(ab). dom(ac). dom(bc). dom(o). dom(oa). dom(ob). dom(oc). dom(a1b1). dom(b1c1). dom(a1c1). dom(a2b2). dom(b2c2). dom(a2c2). _ axiom goal_normal(U) : (l(U,U),i(bc,U),i(ac,U),i(ab,U) => goal). _ axiom t1in2 : (i(a1,b2c2),i(b1,a2c2),i(c1,a2b2) => goal). _ axiom t2in1 : (i(a2,b1c1),i(b2,a1c1),i(c2,a1b1) => goal). _ axiom gap_a : (true => i(a1,b2c2);i(b2,a1c1)). _ axiom gap_b : (true => i(b1,a2c2);i(c2,a1b1)). _ axiom gap_c : (true => i(c1,a2b2);i(a2,b1c1)). %Desargues assumptions: points, lines and incidences %triangles a1b1c1 and a2b2c2 _ axiom ia1b1 : (true => i(a1,a1b1)). _ axiom ib1a1 : (true => i(b1,a1b1)). _ axiom ia2b2 : (true => i(a2,a2b2)). _ axiom ib2a2 : (true => i(b2,a2b2)). _ axiom ia1c1 : (true => i(a1,a1c1)). _ axiom ic1a1 : (true => i(c1,a1c1)). _ axiom ia2c2 : (true => i(a2,a2c2)). _ axiom ic2a2 : (true => i(c2,a2c2)). _ axiom ic1b1 : (true => i(c1,b1c1)). _ axiom ib1c1 : (true => i(b1,b1c1)). _ axiom ic2b2 : (true => i(c2,b2c2)). _ axiom ib2c2 : (true => i(b2,b2c2)). % lines through perspectivity point o and corresponding vertices _ axiom iooa : (true => i(o,oa)). _ axiom ioob : (true => i(o,ob)). _ axiom iooc : (true => i(o,oc)). _ axiom ia1oa : (true => i(a1,oa)). _ axiom ia2oa : (true => i(a2,oa)). _ axiom ib1ob : (true => i(b1,ob)). _ axiom ib2ob : (true => i(b2,ob)). _ axiom ic1oc : (true => i(c1,oc)). _ axiom ic2oc : (true => i(c2,oc)). % cross b1c1,b2c2 in point bc _ axiom ibc1 : (true => i(bc,b1c1)). _ axiom ibc2 : (true => i(bc,b2c2)). % cross a1c1, a2c2 in point ac _ axiom iac1 : (true => i(ac,a1c1)). _ axiom iac2 : (true => i(ac,a2c2)). % cross a1b1,a2b2 in point ab _ axiom iab1 : (true => i(ab,a1b1)). _ axiom iab2 : (true => i(ab,a2b2)). %to prove: points ab,bc,ac on (perspectivity) line %triangle1 non-degenerate _ axiom triangle1(L) : (i(a1,L),i(b1,L),i(c1,L) => false). %triangle2 non-degenerate _ axiom triangle2(L) : (i(a2,L),i(b2,L),i(c2,L) => false). %no corresponding vertices in common _ axiom notaa : (p(a2,a1)=>false). _ axiom notbb : (p(b2,b1)=>false). _ axiom notcc : (p(c2,c1)=>false). %no corresponding edges in common _ axiom notbc : (l(b1c1,b2c2)=>false). _ axiom notac : (l(a1c1,a2c2)=>false). _ axiom notab : (l(a1b1,a2b2)=>false). %pequality for points _ axiom pref(P,L) : (i(P,L) => p(P,P)). %sorted incidence _ axiom psym(P,Q) : (p(P,Q) => p(Q,P)). _ axiom ptra(P,Q,R) : (p(P,Q),p(Q,R) => p(P,R)). %pequality for lines _ axiom lref(P,L) : (i(P,L) => l(L,L)). %sorted incidence _ axiom lsym(L,M) : (l(L,M) => l(M,L)). _ axiom ltra(L,M,N) : (l(L,M),l(M,N) => l(L,N)). %congruence _ axiom pcon(P,Q,L) : (p(P,Q),i(Q,L) => i(P,L)). _ axiom lcon(P,L,M) : (i(P,L),l(L,M) => i(P,M)). %projective uniqueness _ axiom unique(P,Q,L,M) : (i(P,L),i(P,M),i(Q,L),i(Q,M) => p(P,Q);l(L,M)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%proof script%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %not necessary