Propositional Logic Subformula in Prolog

Question

This is a prolog program which defines the syntax of propositional logic

So I'm stuck trying to find where X is a sub formula of Y. I have made the following predicates but I am having problems with this one. Not exactly sure what to do after. I know that I need to check whether X and Y are formulas, but I don't understand the next step.

at(a). % Our first atom.
at(b). % Our second atom.
%fmla shows if it is a formula or not
fmla(X):- at(X). % an atom is a formula
fmla(neg(X)) :- fmla(X). % neg(F) is a formula if F is a formula
fmla(or(X,Y)) :- fmla(X), fmla(Y). % or(F,G) is a formula if F and G are formulas
fmla(and(X,Y)) :- fmla(X), fmla(Y). % and(F,G) is a formula if F and G are formulas
fmla(imp(X,Y)) :- fmla(neg(X)), fmla(Y). %imp is a formula when not F and G are formulas
fmla(iff(X,Y)) :- fmla(imp(X,Y)), fmla(imp(Y,X)). %Double implication

sub(X,Y) :- fmla(X), fmla(Y). 

Would like some ideas of how to solve the sub formula part.

Answer 1

Just describe what qualifies as a subformula:

sub(X,X) :-           % any formula X is a trivial subformula of itself
    fmla(X).
sub(neg(X),Y) :-      % the argument of neg is a subformula
    sub(X,Y).
sub(or(X,_Y),Z) :-    % the 1st arg. of or is a subformula
    sub(X,Z).
sub(or(_X,Y),Z) :-    % the 2nd arg. of or is a subformula
    sub(Y,Z).
sub(and(X,_Y),Z) :-   % 1st arg. of and
    sub(X,Z).
sub(and(_X,Y),Z) :-   % 2nd arg. of and
    sub(Y,Z).
sub(imp(X,_Y),Z) :-   % you see the pattern, right?
    sub(X,Z).
sub(imp(_X,Y),Z) :-
    sub(Y,Z).
sub(iff(X,_Y),Z) :-
    sub(X,Z).
sub(iff(_X,Y),Z) :-
    sub(Y,Z).

Now you can either test whether some formula is a subformula of another:

   ?- sub(and(a,b),b).
yes

or find all subformulas of a given formula:

   ?- sub(neg(or(a,and(neg(a),imp(b,iff(b,a))))),X).
X = neg(or(a,and(neg(a),imp(b,iff(b,a))))) ? ;
X = or(a,and(neg(a),imp(b,iff(b,a)))) ? ;
X = a ? ;
X = and(neg(a),imp(b,iff(b,a))) ? ;
X = neg(a) ? ;
X = a ? ;
X = imp(b,iff(b,a)) ? ;
X = b ? ;
X = iff(b,a) ? ;
X = b ? ;
X = a ? ; 
no

Note that the atoms a and b are listed as often as they occur in the given formula. The same happens for subformulas that occur more than once:

   ?- sub(or(neg(a),neg(a)),X).
X = or(neg(a),neg(a)) ? ;
X = neg(a) ? ;
X = a ? ;
X = neg(a) ? ;
X = a ? ;
no

To get a list of all subformulas without duplicates you can use setof/3:

   ?- setof(X,sub(or(neg(a),neg(a)),X),Sub).
Sub = [a,neg(a),or(neg(a),neg(a))]