Prolog - formulas in propositional logic

Question

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 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?

Answer 1

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.