name(pdc). :- 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_ax(U) : (l(U,U),i(bc,U),i(ac,U),i(ab,U) => goal). _ axiom gap_t1in2 : (true => i(a1,b2c2),i(b1,a2c2),i(c1,a2b2)). %Desargues assumptions: points, lines and incidences %triangles a1b1c1 and a2b2c2 0 axiom ia1b1 : (true => i(a1,a1b1)). 0 axiom ib1a1 : (true => i(b1,a1b1)). 0 axiom ia2b2 : (true => i(a2,a2b2)). 0 axiom ib2a2 : (true => i(b2,a2b2)). 0 axiom ia1c1 : (true => i(a1,a1c1)). 0 axiom ic1a1 : (true => i(c1,a1c1)). 0 axiom ia2c2 : (true => i(a2,a2c2)). 0 axiom ic2a2 : (true => i(c2,a2c2)). 0 axiom ic1b1 : (true => i(c1,b1c1)). 0 axiom ib1c1 : (true => i(b1,b1c1)). 0 axiom ic2b2 : (true => i(c2,b2c2)). 0 axiom ib2c2 : (true => i(b2,b2c2)). % lines through perspectivity point o and corresponding vertices 0 axiom iooa : (true => i(o,oa)). 0 axiom ioob : (true => i(o,ob)). 0 axiom iooc : (true => i(o,oc)). 0 axiom ia1oa : (true => i(a1,oa)). 0 axiom ia2oa : (true => i(a2,oa)). 0 axiom ib1ob : (true => i(b1,ob)). 0 axiom ib2ob : (true => i(b2,ob)). 0 axiom ic1oc : (true => i(c1,oc)). 0 axiom ic2oc : (true => i(c2,oc)). % cross b1c1,b2c2 in point bc 0 axiom ibc1 : (true => i(bc,b1c1)). 0 axiom ibc2 : (true => i(bc,b2c2)). % cross a1c1, a2c2 in point ac 0 axiom iac1 : (true => i(ac,a1c1)). 0 axiom iac2 : (true => i(ac,a2c2)). % cross a1b1,a2b2 in point ab 0 axiom iab1 : (true => i(ab,a1b1)). 1 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)). %projective geometry line(P,Q,L) axiom line(P,Q) : (p(P,P),p(Q,Q) => dom(L),i(P,L),i(Q,L)). point(L,M,P) axiom point(L,M) : (l(L,L),l(M,M) => dom(P),i(P,L),i(P,M)). %Pappus: A,B,C on L, D,E,F on M, then ... or N=O;P=Q;R=S pappus(G,H,I) axiom papp(A,B,C,D,E,F,G,H,I,L,M,N,O,P,Q,R,S) : ( i(A,L),i(B,L),i(C,L),i(D,M),i(E,M),i(F,M), % ABC on L, DEF on M i(B,N),i(F,N),i(G,N),i(C,O),i(E,O),i(G,O), % cross BF,CE in G i(B,P),i(D,P),i(H,P),i(A,Q),i(E,Q),i(H,Q), % cross BD,AE in H i(C,R),i(D,R),i(I,R),i(A,S),i(F,S),i(I,S) % cross CD,AF in I => l(N,O);l(P,Q);l(R,S); % degenerations dom(T),l(T,T),i(G,T),i(H,T),i(I,T)). % G,H,I on line T %%%%%%%%%%%%%%%%%%%%%%%%%%%%%proof script%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% next(0,[],[]). next(1,[],[ line(ac,b2,L0), point(L0,oa,P1), point(L0,oc,P2), pappus(a2,bc,P2), pappus(c2,ab,P1), pappus(ab,bc,ac) ]). next(H,[H|T],T). enabled(0,[]). enabled(1,[]). enabled(H,[H|T]):-write(H),nl.