Aussagenlogik Teilformel in Prolog

Question

Dies ist ein Prolog-Programm, das die Syntax der Aussagenlogik definiert

So versuche ich bin fest zu finden, wo X eine Unterformel von Y. ist Ich habe die folgenden Prädikate gemacht, aber ich bin Probleme mit diesem haben. Ich bin mir nicht sicher, was ich danach machen soll. Ich weiß, dass ich überprüfen muss, ob X und Y Formeln sind, aber ich verstehe den nächsten Schritt nicht.

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). 

Ich möchte einige Ideen, wie Sie die Subformel Teil lösen.

Answer 1

nur beschreiben, was als Teilformel qualifiziert:

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). 

Jetzt können Sie entweder testen, ob einige Formel ein Teilformel eines anderen ist:

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

oder alle Teilformeln einer bestimmten Formel finden:

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

Beachten Sie, dass die Atome a und b so oft aufgelistet sind, wie sie in der gegebene Formel. Das gleiche geschieht für Teilformeln, die mehr als einmal vorkommen:

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

Um eine Liste aller Teilformeln ohne Duplikate erhalten Sie SETOF/3 verwenden können:

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