/* SKOLEM.

Skolem Normal Form Procedure
(FORMUL contains test examples)

Alan Bundy 17.3.79 */


/*operator declarations*/

:- op(400,xfy,;).               % Disjunction

:- op(300,xfy,<->).             % Double Implication

:-op(400,xfy,->).               % Implication


/*skolem normal form*/

skolem(Sentence,NormalForm) :- !,               % Normal calling pattern
        skolem(Sentence,NormalForm,[],0).       % assume no free vars and being asserted


skolem(P <-> Q, (P1->Q1)&(Q1->P1),Vars,Par) :- !,       % Double implication
        skolem(P,P1,Vars,Par), skolem(Q,Q1,Vars,Par).

skolem(all(X,P),P1,Vars,0) :- !,                % Universal quantification
        skolem(P,P1,[X|Vars],0).

skolem(all(X,P),P2,Vars,1) :- !,                % Universal quantification
        gensym(f,Fs), univ(Fs,Vars,F),          % dual case
        subst(X=F,P,P1),
        skolem(P1,P2,Vars,1).

skolem(some(X,P),P2,Vars,0) :- !,               % Existential quantification
        gensym(f,Fs), univ(Fs,Vars,F),
        subst(X=F,P,P1),
        skolem(P1,P2,Vars,0).

skolem(some(X,P),P1,Vars,1) :- !,               % Existential quantification
        skolem(P,P1,[X|Vars],1).                % dual case

skolem(P->Q,P1->Q1,Vars,Par) :- !,                      % Implication
        opposite(Par,Par1), skolem(P,P1,Vars,Par1),
        skolem(Q,Q1,Vars,Par).

skolem(P;Q,P1;Q1,Vars,Par) :- !,                        % Disjunction
        skolem(P,P1,Vars,Par), skolem(Q,Q1,Vars,Par).

skolem(P&Q,P1&Q1,Vars,Par) :- !,                        % Conjunction
        skolem(P,P1,Vars,Par), skolem(Q,Q1,Vars,Par).

skolem(not P,not P1,Vars,Par) :- !,                     % Negation
        opposite(Par,Par1), skolem(P,P1).

skolem(Pred,Pred,Vars,Par) :- !.                % Atomic formula


/*opposite parities*/

opposite(0,1).
opposite(1,0).

/*univ - apply args to symbol*/
univ(Fs,Vars,F) :- !,
        F =.. [Fs|Vars].


/* MINI-PROJECTS

1. Try out on various formulae.

2. Modify the program to deal with bounded quantification, e.g.
all_in(X,Set,P) - meaning, for all X in Set, P is true.

3.  Build programs for putting formulae in:  (a) Prenex Normal Form, (b)
Conjunctive Normal Form, as per section 5.2 of 'Artificial
Mathematicians'. You may wish to use file REWRIT.

*/