Prolog - formulas in propositional logic

I am trying to make a predicate in order to validate if a given input represents a formula.

I am allowed to use only to propositional atoms like p, q, r, s, t, etc. The formulas which I have to test are the following:

neg(X) - represents the negation of X  
and(X, Y) - represents X and开发者_JAVA技巧 Y  
or(X, Y) - represents X or Y  
imp(X, Y) - represents X implies Y  

I have made the predicate wff which returns true if a given structure is a formula and false the otherwise. Also, I don't have to use variables inside the formula, only propositional atoms as mentioned bellow.

logical_atom( A ) :-
    atom( A ),     
    atom_codes( A, [AH|_] ),
    AH >= 97,
    AH =< 122.

wff(A):-
    \+ ground(A),
    !,
    fail.

wff(and(A, B)):-
    wff(A),
    wff(B).

wff(neg(A)):-
    wff(A).

wff(or(A, B)):-
    wff(A),
    wff(B).

wff(imp(A, B)):-
    wff(A),
    wff(B).

wff(A):-
    ground(A),
    logical_atom(A),
    !.

When i introduce a test like this one, wff(and(q, imp(or(p, q), neg(p))))., the call returns both the true and false values. Can you please tell me why it happens like this?

The data structure you chose to represent formulae is called "defaulty", because you need a "default" case to test for atomic identifiers: Everything that is not something of the above (and, or, neg, imp) and satisfies logical_atom/1 is a logical atom (in your representation). The interpreter cannot distinguish these cases by their functor to apply first-argument indexing. It is much cleaner to, in analogy to and/or/etc., also equip atomic variables with their dedicated functor, say "atom(...)". wff/1 could then read:

wff(atom(_)).
wff(and(A, B))    :- wff(A), wff(B).
wff(neg(A))       :- wff(A).
wff(or(A, B))     :- wff(A), wff(B).
wff(imp(A, B))    :- wff(A), wff(B).

Your query is now deterministic as desired:

?- wff(and(atom(q), imp(or(atom(p), atom(q)), neg(atom(p))))).
true.

If your formulae are initially not represented in this way, it is still better to first convert them to such a form, and then to use such a representation which is not defaulty for further processing.

An additional advantage is that you can now easily not only test but also enumerate well-formed formulae with code like:

wff(atom(_))  --> [].
wff(and(A,B)) --> [_,_], wff(A), wff(B).
wff(neg(A))   --> [_], wff(A).
wff(or(A,B))  --> [_,_], wff(A), wff(B).
wff(imp(A,B)) --> [_,_], wff(A), wff(B).

And a query like:

?- length(Ls, _), phrase(wff(W), Ls), writeln(W), false.

Yielding:

atom(_G490)
neg(atom(_G495))
and(atom(_G499),atom(_G501))
neg(neg(atom(_G500)))
or(atom(_G499),atom(_G501))
imp(atom(_G499),atom(_G501))
and(atom(_G502),neg(atom(_G506)))
and(neg(atom(_G504)),atom(_G506))
neg(and(atom(_G504),atom(_G506)))
neg(neg(neg(atom(_G505))))
neg(or(atom(_G504),atom(_G506)))
neg(imp(atom(_G504),atom(_G506)))
etc.

as its output.