% p(n) iff not p(k) for all k>n leads to a contradiction % it suffices that the domain is non-empty and < is transitive and serial name(ser). :- dynamic p/1,notp/1,less/2. % domain element o dom(o). % the systematic translation based on the tableaux method yields: _ axiom left_to_right(X,Y): (p(X),less(X,Y),p(Y) => false). _ axiom right_to_left(X): (dom(X) => p(X);dom(Y),less(X,Y),p(Y)). % basic facts on less _ axiom transitive_less(X,Y,Z) :(less(X,Y),less(Y,Z) => less(X,Z)). _ axiom serial_less(X) :(dom(X) => dom(Y),less(X,Y)). % last! % NB inconsistency is proved without a clause for goal!