The following is all the Prolog code from
"First-Order Logic and Automated Theorem Proving"
Second Edition
by Melvin Fitting
Springer 1996

Each portion is identified by a marker at the beginning,
of the form:
**-----------------Page numbers-----------------------

**-----------------36 to 39---------------------------
/*  Dual 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]).

/*  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 occurrences of
      Item from List.
*/

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

/*  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 _).

/*  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 _)).

/*  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 the components
      of the formula X, as defined in the alpha and
      beta table.
*/

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

/*  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 generalized disjunction of generalized
      conjunctions.
*/

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),
  Newcon = [Alphaone, Alphatwo | Temporary],
  New = [Newcon | Rest].

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

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

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

expand(Dis, Newdis) :-
  singlestep(Dis, Temp),
  expand(Temp, Newdis).

expand(Dis, Dis).

/*  dualclauseform(X, Y) :- Y is the dual clause form of X.
*/

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

**-----------------47 to 47---------------------------
/*  closed(Tableau) :- every branch of Tableau contains a
        contradiction.
*/

closed([Branch | Rest]) :-
  member(false, Branch),
  closed(Rest).

closed([Branch | Rest]) :-
  member(X, Branch),
  member(neg X, Branch),
  closed(Rest).

closed([ ]).

**-----------------48 to 48---------------------------
/*  test(X) :- create a complete tableau expansion
        for neg X, and see if it is closed.
*/

test(X) :-
  expand([[neg X]], Y),
  closed(Y).

**-----------------48 to 48---------------------------
test(X) :-
  expand([[neg X]], Y),
  !,
  closed(Y).

**-----------------48 to 48---------------------------
 /*  if_then_else(P, Q, R) :-
        either P and Q, or not P and R.
*/

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

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

**-----------------48 to 49---------------------------
/*  test(X) :- create a complete tableau expansion
        for neg X, if it is closed, say we have a
        proof, otherwise, say we don't.
*/

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

yes :- write('Propositional tableau theorem'), nl.

no :- write('Not a propositional tableau theorem'), nl.

**-----------------49 to 49---------------------------
/*  expand_and_close(Tableau) :-
      some expansion of Tableau closes.
*/

expand_and_close(Tableau) :-
  closed(Tableau).

expand_and_close(Tableau) :-
  singlestep(Tableau, Newtableau), !,
  expand_and_close(Newtableau).

**-----------------50 to 50---------------------------
/*  test(X) :- create a tableau expansion for neg X,
        if it is closed, say we have a proof,
        otherwise, say we don't.
*/

test(X) :-
  if_then_else(expand_and_close([[neg X]]), yes, no).

**-----------------161 to 161-------------------------
/*  variable(X) :- X is a free variable.
*/

variable(var(_)).

**-----------------162 to 162-------------------------
/*  partialvalue(X, Env, Y) :-
      Y is the partially evaluated value of term X
      in environment Env.
*/

partialvalue(X, Env, Y) :-
   member([X,Z], Env),
   partialvalue(Z, Env, Y).

partialvalue(X, Env, X).

/*  member(X, Y) :- X is a member of the list Y.
*/

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

**-----------------162 to 162-------------------------
/*  in(X, T, Env) :-
      X occurs in term T, evaluated in environment Env.
*/

in(X, T, Env) :-
   partialvalue(T, Env, U),
   ( X == U;
     not variable(U), not atomic(U), infunctor(X, U, Env)
   ).

infunctor(X, U, Env) :-
   U =.. [_|L],
   inlist(X, L, Env).

inlist(X, [T|_], Env) :-
   in(X, T, Env).

inlist(X, [_|L], Env) :-
   inlist(X, L, Env).

**-----------------163 to 164-------------------------
/*  unify(Term1, Term2, Env, Newenv) :-
      Unifying Term1 and Term2 in environment Env
      produces the new environment Newenv.
*/

unify(Term1, Term2, Env, Newenv) :-
   partialvalue(Term1, Env, Val1),
   partialvalue(Term2, Env, Val2),
   (
     (Val1==Val2, Newenv = Env);
     (variable(Val1), not in(Val1, Val2, Env),
        Newenv=[ [Val1, Val2] | Env] );
     (variable(Val2), not in(Val2, Val1, Env),
        Newenv=[ [Val2, Val1] | Env] );
     (not variable(Val1), not variable(Val2),
        not atomic(Val1), not atomic(Val2),
        unifyfunctor(Val1, Val2, Env, Newenv) )
   ).

/*  unifyfunctor(Fun1, Fun2, Env, Newenv) :-
      Unifying the functors Fun1 and Fun2 in
      environment Env produces environment Newenv.
*/

unifyfunctor(Fun1, Fun2, Env, Newenv) :-
   Fun1 =.. [FunSymb | Args1],
   Fun2 =.. [FunSymb | Args2],
   unifylist(Args1, Args2, Env, Newenv).

/*  unifylist(List1, List2, Env, Newenv) :-
      Starting in environment Env and
      unifying each term in List1 with the
      corresponding term in List2 produces
      the environment Newenv.
*/

unifylist([ ], [ ], Env, Env).

unifylist([Head1 | Tail1], [Head2 | Tail2], Env, Newenv) :-
   unify(Head1, Head2, Env, Temp),
   unifylist(Tail1, Tail2, Temp, Newenv).

**-----------------164 to 165-------------------------
/*  unify(Term1, Term2) :-
       Term1 and Term2 are unified with the occurs check.
       See Sterling and Shapiro, The Art of Prolog.
*/

unify(X,Y) :-
     var(X), var(Y), X=Y.
unify(X,Y) :-
     var(X), nonvar(Y), not_occurs_in(X,Y), X=Y.
unify(X,Y) :-
     var(Y), nonvar(X), not_occurs_in(Y,X), Y=X.
unify(X,Y) :-
     nonvar(X), nonvar(Y), atomic(X), atomic(Y), X=Y.
unify(X,Y) :-
     nonvar(X), nonvar(Y),
     compound(X), compound(Y),
     term_unify(X,Y).

not_occurs_in(X,Y) :-
     var(Y), X \== Y.
not_occurs_in(X,Y) :-
     nonvar(Y), atomic(Y).
not_occurs_in(X,Y) :-
     nonvar(Y), compound(Y), functor(Y,F,N),
     not_occurs_in(N,X,Y).

not_occurs_in(N,X,Y) :-
     N>0, arg(N,Y,Arg), not_occurs_in(X,Arg), N1 is N-1,
     not_occurs_in(N1,X,Y).
not_occurs_in(0,X,Y) .

term_unify(X,Y) :-
     functor(X,F,N), functor(Y,F,N), unify_args(N,X,Y).

unify_args(N,X,Y) :-
     N>0, unify_arg(N,X,Y), N1 is N-1, unify_args(N1,X,Y).
unify_args(0,X,Y).

unify_arg(N,X,Y) :-
     arg(N,X,ArgX), arg(N,Y,ArgY), unify(ArgX,ArgY).

compound(X) :- functor(X,_,N), N>0.

**-----------------169 to 170-------------------------
/*   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
         occurrences of Item from List.
*/

remove(X, [ ], [ ]).
remove(X, [Y | Tail], Newtail) :-
   X == Y,
   remove(X, Tail, Newtail).
remove(X, [Y | Tail], [Y | Newtail]) :-
   X \== Y,
   remove(X, Tail, Newtail).

/*   append(ListA, ListB, Newlist) :-
         Newlist is the result of appending ListA
         and ListB.
*/

append([ ], List, List).
append([Head | Tail], List, [Head | Newlist]) :-
   append(Tail, List, Newlist).

**-----------------170 to 172-------------------------
/*   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]).

/*   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 _).

/*   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 _)).

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

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

/*   binary_operator(X) :- X is a binary operator.
*/

binary_operator(X) :-
   member(X, [and, or, imp, revimp, uparrow, downarrow,
   notimp, notrevimp]).

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

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

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

**-----------------172 to 173-------------------------
/*   universal(X) :- X is a gamma formula.
*/

universal(all(_,_)).
universal(neg some(_,_)).

/*   existential(X) :- X is a delta formula.
*/

existential(some(_,_)).
existential(neg all(_,_)).

/*   literal(X) :- X is a literal.
*/

literal(X) :-
   not conjunctive(X),
   not disjunctive(X),
   not unary(X),
   not universal(X),
   not existential(X).

/*   atomicfmla(X) :- X is an atomic formula.
*/

atomicfmla(X) :-
   literal(X),
   X \= neg _.

**-----------------173 to 174-------------------------
/*   sub(Term, Variable, Formula, NewFormula) :-
         NewFormula is the result of substituting
         occurrences of Term for each free
         occurrence of Variable in Formula.
*/

sub(Term, Variable, Formula, NewFormula) :-
   sub_(Term, Variable, Formula, NewFormula) , !.

sub_(Term, Var, A, Term) :- Var == A.
sub_(Term, Var, A, A) :- atomic(A).
sub_(Term, Var, A, A) :- var(A).

sub_(Term, Var, neg X, neg Y) :-
   sub_(Term, Var, X, Y).

sub_(Term, Var, Binary_One, Binary_Two) :-
   binary_operator(F),
   Binary_One =.. [F, X, Y],
   Binary_Two =.. [F, U, V],
   sub_(Term, Var, X, U),
   sub_(Term, Var, Y, V).

sub_(Term, Var, all(Var, Y), all(Var, Y)).
sub_(Term, Var, all(X, Y), all(X, Z)) :-
   sub_(Term, Var, Y, Z).
sub_(Term, Var, some(Var, Y), some(Var, Y)).
sub_(Term, Var, some(X, Y), some(X, Z)) :-
   sub_(Term, Var, Y, Z).

sub_(Term, Var, Functor, Newfunctor) :- 
   Functor =.. [F | Arglist],
   sub_list(Term, Var, Arglist, Newarglist),
   Newfunctor =.. [F | Newarglist].

sub_list(Term, Var, [Head | Tail], [Newhead | Newtail]) :-
   sub_(Term, Var, Head, Newhead),
   sub_list(Term, Var, Tail, Newtail).

sub_list(Term, Var, [ ], [ ]).

**-----------------174 to 174-------------------------
/*  instance(F, Term, Ins) :-
         F is a quantified formula, and Ins is the result
         of removing the quantifier and replacing all
         free occurrences of the quantified variable by
         occurrences of Term.
*/

instance(all(X,Y), Term, Z) :- sub(Term, X, Y, Z).
instance(neg some(X,Y), Term, neg Z) :- sub(Term, X, Y, Z).
instance(some(X,Y), Term, Z) :- sub(Term, X, Y, Z).
instance(neg all(X,Y), Term, neg Z) :- sub(Term, X, Y, Z).

**-----------------175 to 175-------------------------
/*   funcount(N) :- N is the current Skolem function index.
*/

funcount(1).

/*   newfuncount(N) :-
         N is the current Skolem function index, and as a
         side effect, the remembered value is incremented.
*/

newfuncount(N) :-
   funcount(N),
   retract(funcount(N)),
   M is N+1,
   assert(funcount(M)).

/*   reset :- the Skolem function index is reset to 1.
*/

reset :-
   retract(funcount(_)),
   assert(funcount(1)),
   !.

**-----------------175 to 176-------------------------
/*   sko_fun(X, Y) :-
         X is a list of free variables, and Y is a
         previously unused Skolem function symbol
         applied to those free variables.
*/

sko_fun(Varlist, Skoterm) :-
   newfuncount(N),
   Skoterm =.. [fun | [N | Varlist]].

**-----------------176 to 176-------------------------
/*   notation(Notated, Free) :-
         Notated is a notated formula, and Free is its
         associated free variable list.
*/

notation(n(X, Y), X).

/*   fmla(Notated, Formula) :-
         Notated is a notated formula, and Formula is its
         formula part.
*/

fmla(n(X, Y), Y).

**-----------------178 to 180-------------------------
/*   singlestep(OldTableau, OldQdepth,
            NewTableau, NewQdepth) :-
         the application of one tableau rule to OldTableau,
         with a Q-depth of OldQdepth, will produce the
         tableau NewTableau, and will change the available
         Q-depth to NewQdepth.
*/

singlestep([OldBranch | Rest], Qdepth,
      [NewBranch | Rest], Qdepth) :-
   member(NotatedFormula, OldBranch),
   notation(NotatedFormula, Free),
   fmla(NotatedFormula, Formula),
   unary(Formula),
   component(Formula, NewFormula),
   notation(NewNotatedFormula, Free),
   fmla(NewNotatedFormula, NewFormula),
   remove(NotatedFormula, OldBranch, TempBranch),
   NewBranch = [NewNotatedFormula | TempBranch].

singlestep([OldBranch | Rest], Qdepth,
      [NewBranch | Rest], Qdepth) :-
   member(NotatedAlpha, OldBranch),
   notation(NotatedAlpha, Free),
   fmla(NotatedAlpha, Alpha),
   conjunctive(Alpha),
   components(Alpha, AlphaOne, AlphaTwo),
   notation(NotatedAlphaOne, Free),
   fmla(NotatedAlphaOne, AlphaOne),
   notation(NotatedAlphaTwo, Free),
   fmla(NotatedAlphaTwo, AlphaTwo),
   remove(NotatedAlpha, OldBranch, TempBranch),
   NewBranch =
     [NotatedAlphaOne, NotatedAlphaTwo | TempBranch].

singlestep([OldBranch | Rest], Qdepth,
      [NewBranchOne, NewBranchTwo | Rest], Qdepth) :-
   member(NotatedBeta, OldBranch),
   notation(NotatedBeta, Free),
   fmla(NotatedBeta, Beta),
   disjunctive(Beta),
   components(Beta, BetaOne, BetaTwo),
   notation(NotatedBetaOne, Free),
   fmla(NotatedBetaOne, BetaOne),
   notation(NotatedBetaTwo, Free),
   fmla(NotatedBetaTwo, BetaTwo),
   remove(NotatedBeta, OldBranch, TempBranch),
   NewBranchOne = [NotatedBetaOne | TempBranch],
   NewBranchTwo = [NotatedBetaTwo | TempBranch].

singlestep([OldBranch | Rest], Qdepth,
      [NewBranch | Rest], Qdepth) :-
   member(NotatedDelta, OldBranch),
   notation(NotatedDelta, Free),
   fmla(NotatedDelta, Delta),
   existential(Delta),
   sko_fun(Free, Term),
   instance(Delta, Term, DeltaInstance),
   notation(NotatedDeltaInstance, Free),
   fmla(NotatedDeltaInstance, DeltaInstance),
   remove(NotatedDelta, OldBranch, TempBranch),
   NewBranch = [NotatedDeltaInstance | TempBranch].

singlestep([OldBranch | Rest], OldQdepth,
      NewTree, NewQdepth) :-
   member(NotatedGamma, OldBranch),
   notation(NotatedGamma, Free),
   fmla(NotatedGamma, Gamma),
   universal(Gamma),
   OldQdepth > 0,
   remove(NotatedGamma, OldBranch, TempBranch),
   NewFree = [V | Free],
   instance(Gamma, V, GammaInstance),
   notation(NotatedGammaInstance, NewFree),
   fmla(NotatedGammaInstance, GammaInstance),
   append([NotatedGammaInstance | TempBranch], 
     [NotatedGamma], NewBranch),
   append(Rest, [NewBranch], NewTree),
   NewQdepth is OldQdepth-1.

singlestep([Branch | OldRest], OldQdepth,
      [Branch | NewRest], NewQdepth) :-
   singlestep(OldRest, OldQdepth, NewRest, NewQdepth).

**-----------------180 to 180-------------------------
/*   expand(Tree, Qdepth, Newtree) :-
         the complete expansion of the tableau Tree,
         allowing Qdepth applications of the gamma
         rule, is Newtree.
*/

expand(Tree, Qdepth, Newtree) :-
   singlestep(Tree, Qdepth, TempTree, TempQdepth),
   expand(TempTree, TempQdepth, Newtree).

expand(Tree, Qdepth, Tree).

**-----------------180 to 181-------------------------
/*   unify(Term1, Term2) :-
         Term1 and Term2 are unified with the occurs check.
         See Sterling and Shapiro,
         The Art of Prolog.
*/

unify(X,Y) :-
   var(X), var(Y), X=Y.
unify(X,Y) :-
   var(X), nonvar(Y), not_occurs_in(X,Y), X=Y.
unify(X,Y) :-
   var(Y), nonvar(X), not_occurs_in(Y,X), Y=X.
unify(X,Y) :-
   nonvar(X), nonvar(Y), atomic(X), atomic(Y), X=Y.
unify(X,Y) :-
   nonvar(X), nonvar(Y),
   compound(X), compound(Y),
   term_unify(X,Y).

not_occurs_in(X,Y) :-
   var(Y), X \== Y.
not_occurs_in(X,Y) :-
   nonvar(Y), atomic(Y).
not_occurs_in(X,Y) :-
   nonvar(Y), compound(Y), functor(Y,F,N),
   not_occurs_in(N,X,Y).

not_occurs_in(N,X,Y) :-
   N>0, arg(N,Y,Arg), not_occurs_in(X,Arg), N1 is N-1,
   not_occurs_in(N1,X,Y).
not_occurs_in(0,X,Y) .

term_unify(X,Y) :-
   functor(X,F,N), functor(Y,F,N), unify_args(N,X,Y).

unify_args(N,X,Y) :-
   N>0, unify_arg(N,X,Y), N1 is N-1, unify_args(N1,X,Y).
unify_args(0,X,Y).

unify_arg(N,X,Y) :-
   arg(N,X,ArgX), arg(N,Y,ArgY), unify(ArgX,ArgY).

compound(X) :- functor(X,_,N), N>0.

**-----------------181 to 182-------------------------
/*   closed(Tableau) :- every branch of Tableau can be
        made to contain a contradiction, after a suitable
        free variable substitution.
*/

closed([Branch | Rest]) :-
   member(Falsehood, Branch),
   fmla(Falsehood, false),
   closed(Rest).

closed([Branch | Rest]) :-
   member(NotatedOne, Branch),
   fmla(NotatedOne, X),
   atomicfmla(X),
   member(NotatedTwo, Branch),
   fmla(NotatedTwo, neg Y),
   unify(X, Y),
   closed(Rest).

closed([ ]).

**-----------------182 to 183-------------------------
/*   if_then_else(P, Q, R) :-
         either P and Q, or not P and R.
*/

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

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

/*   test(X, Qdepth) :- create a complete tableau expansion
        for neg X, allowing Qdepth applications of the
        gamma rule.  Test for closure.
*/

test(X, Qdepth) :- 
   reset,
   notation(NotatedFormula, [ ]),
   fmla(NotatedFormula, neg X),
   expand([[NotatedFormula]], Qdepth, Tree),
   if_then_else(closed(Tree), yes(Qdepth), no(Qdepth)).

yes(Qdepth) :-
   write('First-order tableau theorem at Q-depth '),
   write(Qdepth),
   write(.),
   nl.

no(Qdepth) :-
   write('Not a first-order tableau theorem at Q-depth '),
   write(Qdepth),
   write('.'),
   nl.

**-----------------305 to 305-------------------------
?-op(120, xfy, eq).

**-----------------305 to 305-------------------------
/*   not_member(Item, List) :-
         Item does not occur in List, where an
         occurrence must be via identity, not
         via unification.
*/

not_member(_, [ ]).
not_member(Item, [Head | Tail]) :-
   Item \== Head, not_member(Item, Tail).

**-----------------306 to 307-------------------------
/*   replace_term(T, Term, U, NewTerm) :-
         NewTerm is the result of replacing one
         occurrence of T in Term (after a unification)
         with an occurrence of U.
*/

replace_term(T, Term, U, NewTerm) :-
   unify(T, Term),
   unify(U, NewTerm).

replace_term(T, Term, U, NewTerm) :-
   compound(Term),
   Term =.. [F | Args],
   replace_term_list(T, Args, U, NewArgs),
   NewTerm =.. [F | NewArgs].

/*   replace_term_list(T, OldList, U, NewList) :-
         OldList is a list of terms, and NewList
         is the result of applying replace_term
         to one of them, replacing T by U.
*/

replace_term_list(T, [First | Rest], 
   U, [NewFirst | Rest]) :-
      replace_term(T, First, U, NewFirst).

replace_term_list(T, [First | Rest], 
   U, [First | NewRest]) :-
      replace_term_list(T, Rest, U, NewRest).

**-----------------307 to 307-------------------------
/*   replace_atomic(T, Atomic, U, NewAtomic) :-
         NewAtomic is the result of replacing one 
         occurrence of the term T in the atomic formula
         Atomic with an occurrence of U.
*/

replace_atomic(T, Atomic, U, NewAtomic):-
   atomicfmla(Atomic),
   Atomic =.. [F | Args],
   replace_term_list(T, Args, U, NewArgs),
   NewAtomic =.. [F | NewArgs].

/*   replace_literal(T, Literal, U, NewLiteral) :-
         NewLiteral is the result of replacing one
         occurrence of the term T in the literal
         Literal with an occurrence of U.
*/

replace_literal(T, Atomic, U, NewAtomic) :-
   replace_atomic(T, Atomic, U, NewAtomic).
replace_literal(T, neg Atomic, U, neg NewAtomic) :-
   replace_atomic(T, Atomic, U, NewAtomic).

**-----------------308 to 309-------------------------
/*   reorganize(OldTableau, RDepth, NewTableau) :-
         NewTableau is OldTableau with each branch
         purged of all non-literals, and for each
         notated literal, the notation is changed
         to RDepth.
*/

reorganize([ ], _, [ ]).

reorganize([OldBranch | Rest], RDepth,
     [NewBranch | NewRest]) :-
   modifybranch(OldBranch, RDepth, NewBranch),
   reorganize(Rest, RDepth, NewRest).

/*   modifybranch(OldBranch, RDepth, NewBranch) :-
         NewBranch is OldBranch with each non-literal
         removed, and for each notated literal, the
         notation is changed to RDepth.
*/

modifybranch([ ], _, [ ]).

modifybranch([NotatedLiteral | Rest], RDepth,
     [NewNotatedLiteral | NewRest]) :-
   fmla(NotatedLiteral, Literal),
   literal(Literal),
   fmla(NewNotatedLiteral, Literal),
   notation(NewNotatedLiteral, RDepth),
   modifybranch(Rest, RDepth, NewRest).

modifybranch([NonNotatedLiteral | Rest], RDepth,
     NewRest) :-
   modifybranch(Rest, RDepth, NewRest).

**-----------------309 to 310-------------------------
closed([Branch | Rest]) :-
   member(Notated, Branch),
   fmla(Notated, neg X eq Y),
   unify(X, Y),
   closed(Rest).

**-----------------310 to 310-------------------------
closed([OldBranch | Rest]) :-
   member(NotatedEquality, OldBranch),
   fmla(NotatedEquality, X eq Y),
   member(NotatedLiteral, OldBranch),
   notation(NotatedLiteral, RDepth),
   RDepth > 0,
   fmla(NotatedLiteral, Literal),
   replace_literal(X, Literal, Y, NewLiteral),
   NewRDepth is RDepth - 1,
   fmla(NewNotatedLiteral, NewLiteral),
   notation(NewNotatedLiteral, NewRDepth),
   fmla(RevisedNotatedLiteral, Literal),
   notation(RevisedNotatedLiteral, NewRDepth),
   remove(NotatedLiteral, OldBranch, TempBranch),
   NewBranch = [NewNotatedLiteral, RevisedNotatedLiteral |
     TempBranch],
   closed([NewBranch | Rest]).

**-----------------310 to 311-------------------------
/*   test(X, Qdepth, RDepth) :- create a complete tableau
         expansion for neg X, allowing Qdepth applications
         of the gamma rule, but no equality rules.  Then
         reorganize the tableau and test for closure,
         allowing the equality replacement rule to be
         used RDepth times on each formula.
 
     Note that this replaces the earlier test predicate.
*/

test(X, Qdepth, RDepth) :-
   reset,
   notation(NotatedFormula, [ ]),
   fmla(NotatedFormula, neg X),
   expand([[NotatedFormula]], Qdepth, Tree), !,
   reorganize(Tree, RDepth, NewTree), !,
   if_then_else(closed(NewTree), 
      yes(Qdepth, RDepth), no(Qdepth, RDepth)),
   !, fail.

yes(Qdepth, RDepth) :-
   write('Theorem at Q-depth '),
   write(Qdepth),
   write(' and R-depth '),
   write(RDepth),
   write('.'),
   nl.

no(Qdepth, RDepth) :-
   write('Not a theorem at Q-depth '),
   write(Qdepth),
   write(' and R-depth '),
   write(RDepth),
   write('.'),
   nl.