Resolution Prover

/* 	Clause Form Program

	Propositional operators are: neg, and, or, imp, revimp, uparrow, downarrow, notimp, and notrevimp.
*/

?-op(140, fy, neg).
?-op(160, xfy, [and, or, imp, revimp, uparrow, downarrow, notimp, notrevimp, equiv, notequiv]).

/*	member(Item, List) :- Item occurs in List.
*/

member(X, [X | _]).
member(X, [_ | Tail]) :- member(X, Tail).

/* 	remove(Item, List, Newlist) :-
		Newlist is the result of removing all occurenves of Item from List.
*/

remove(_, [], []).
remove(X, [X | Tail], Newtail) :-
    remove(X, Tail, Newtail).
remove(X, [Head | Tail], [Head | Newatil]) :-
    remove(X, Tail, Newatil).

/*	conjunctive(X) :- X is an alpha-formula.
*/

conjunctive(_ and _).
conjunctive(neg (_ or _)).
conjunctive(neg (_ imp _)).
conjunctive(neg (_ revimp _)).
conjunctive(neg (_ uparrow _)).
conjunctive(_ downarrow _).
conjunctive(_ notimp _).
conjunctive(_ notrevimp _).

/* Extras for equiv and notequiv. */

conjunctive(_ equiv _).
conjunctive(neg (_ notequiv _)).

/* disjunctive(X) :- X is a beta-formula.
*/

disjunctive(neg (_ and _)).
disjunctive(_ or _).
disjunctive(_ imp _).
disjunctive(_ revimp _).
disjunctive(_ uparrow _).
disjunctive(neg (_ downarrow _)).
disjunctive(neg (_ notimp _)).
disjunctive(neg (_ notrevimp _)).

/*	Extras. */

disjunctive(neg (_ equiv _)).
disjunctive(_ notequiv _).

/*	unary(X) :- X is a double negation or a negated constant.
*/

unary(neg neg _).
unary(neg true).
unary(neg false).

/* components(X, Y, Z) :- Y and Z are components of the formula X as defined in the alpha/beta table (FOR CNF).
*/

components(X and Y, X, Y).
components(neg (X and Y), neg X, neg Y).

components(X or Y, X, Y).
components(neg (X or Y), neg X, neg Y).

components(X imp Y, neg X, Y).
components(neg (X imp Y), X, neg Y).

components(X revimp Y, X, neg Y).
components(neg (X revimp Y), neg X, Y).

components(X uparrow Y, neg X, neg Y).
components(neg (X uparrow Y), X, Y).

components(X downarrow Y, neg X, neg Y).
components(neg (X downarrow Y), X, Y).

components(X notimp Y, X, neg Y).
components(neg (X notimp Y), neg X, Y).

components(X notrevimp Y, neg X, Y).
components(neg (X notrevimp Y), X, neg Y).

/*	Extras for equiv and notequiv. */

components(X equiv Y, neg X or Y, neg Y or X).
components(neg (X equiv Y), neg X and Y, neg Y and X).

components(X notequiv Y, neg X and Y, neg Y and X).
components(neg (X notequiv Y), neg X or Y, neg Y or X).

/*	component(X, Y) :- Y is the component of the UNARY formula X.
*/

component(neg neg X, X).
component(neg true, false).
component(neg false, true).

/*	singlestep(Old, New) :- New is the result of applying a single step of the expansion process to Old,
		which is a CONJUNCTION of DISJUNCTIONS.
*/

singlestep([Conjunction | Rest], New) :-
    member(Formula, Conjunction),
    unary(Formula),
    component(Formula, Newformula),
    remove(Formula, Conjunction, Temporary),
    Newconjunction = [Newformula | Temporary],
    New = [Newconjunction | Rest].

singlestep([Conjunction | Rest], New) :-
    member(Alpha, Conjunction),
    conjunctive(Alpha),
    components(Alpha, Alphaone, Alphatwo),
    remove(Alpha, Conjunction, Temporary),
    Newconone = [Alphaone | Temporary],
    Newcontwo = [Alphatwo | Temporary],
    New = [Newconone, Newcontwo | Rest].

singlestep([Conjunction | Rest], New) :-
    member(Beta, Conjunction),
    disjunctive(Beta),
    components(Beta, Betaone, Betatwo),
    remove(Beta, Conjunction, Temporary),
    Newcon = [Betaone, Betatwo | Temporary],
    New = [Newcon | Rest].

singlestep([Conjunction | Rest], [Conjunction | Newrest]) :-
    singlestep(Rest, Newrest).

/* Resolution steps */

resolutionstep(Conjunction, New) :-
    member(Disone, Conjunction),
    member(X, Disone),
    remove(Disone, Conjunction, Newcon),
    remove(X, Disone, Disonenew),

    member(Distwo, Newcon),
    member(neg X, Distwo),
    remove(Distwo, Newcon, Newercon),
    remove(neg X, Distwo, Distwonew),

    New = [Disonenew, Distwonew | Newercon].

resolutionstep([Disjunction | Rest], New) :-
    member(false, Disjunction),
    remove(false, Disjunction, Temp),
    New = [Temp | Rest].

resolutionstep([Conjunction | Rest], [Conjunction | Newrest]) :-
    resolutionstep(Rest, Newrest).

/*	Resolution initialiser. */

resolve(Con, Newcon) :-
    resolutionstep(Con, Temp),
    resolve(Temp, Newcon).

resolve(Con, Con).

/*	expand(Old, New) :- New is the result of applying singlestep to Old, as many times as possible.
*/

expand(Con, Newcon) :-
    singlestep(Con, Temp),
    expand(Temp, Newcon).

expand(Con, Con).

/*	clauseform(X, Y) :- Y is the CNF form of X.
*/

clauseform(X, Y) :- expand([[X]], Y).

/* Check a resolved conjunction for closure. */

closed(Con) :-
    member([], Con).

/* if_then_else(P, Q, R) :- either P and Q, or neg P and R. */

if_then_else(P, Q, R) :- P, !, Q.
if_then_else(P, Q, R) :- R.

/* Test the input and give the appropriate output. */

yes :- write('YES'), nl.
no  :- write('NO'),  nl.

test(X) :-
    expand([[neg X]], Y),
    resolve(Y, Z),
    if_then_else(closed(Z), yes, no).