8.1.8 Two Connectives
Rewriting formulae in Prolog.
Notice that we've only discussed (and in fact that we've only implemented) tableaux rules for the connectives 
and 
so far. This made things simpler for us, and as you probably know it is always possible to treat all other connectives as defined in terms of these two.
We will now give an implementation of the predicate naonly/2 that takes a formula which uses the full set of connectives to an equivalent one that uses only and . All we have to do is to replace the defined connectives according to their definitions:
naonly(~(X),~(Z)) :-
!,naonly(X,Z).
naonly(X & Y, Z & W) :-
!,naonly(X,Z),
naonly(Y,W).
naonly(X v Y,~(~(Z) & ~(W))) :-
!,naonly(X,Z),
naonly(Y,W).
naonly(X > Y,~(Z & ~(W))) :-
!,naonly(X,Z),
naonly(Y,W).
naonly(X,X) :- !.We have to use cuts in the first clauses because we don't want to allow backtracking to the last one (which always matches). If we didn't, we would get additional spurious solutions with only parts of the input formula converted.