% File : CLAUSE
% Author : R.A.O'Keefe
% Updated: 10 March 1984
% Purpose: Convert a formula in FOPC to clausal form.
% Needs : ord_union/3 from UTIL:ORDSET.PL.
/*
This module has three entry points:
clausal_form(Formula, Clauses)
clausal_form_of_negation(Formula, Clauses)
units_separated(Clauses, PosUnits, NegUnits, NonUnits)
The Formula is an , where
::= all(, )
 some(, )
 =>
 <=>
 if(,,)
 and
 or
 ~

::= (,...,)
::=

 (,...,)
The Clauses are a sentence, where
::= [] (true)
 . (and)
::= clause(, )
::= []  .
Note that this representation of a clause is not quite the
usual one. clause([a,b,c], [d,e,f]) represents
a v b v c < d & e & f
or, if you don't like "Kowalski form",
a v b v c v ~d v ~e v ~f
The reason for the two entry points is that the formula may
contain free variables, these are to be understood as being
universally quantified, and the negation of the universal
closure of a formula is not at all the same thing as the
universal closure of the negation!
units_separated takes a list of clauses such as the other two predicates
might produce, and separates them into a list of positive unit clauses
(represented just by s), a list of negative unit clauses (also
represented by their single s), and a list of nonunit clauses.
Some theorem provers might find this separation advantageous, but it is
not buillt into clausal_form becauses some provers would not benefit.
*/
: public
clausal_form/2,
clausal_form_of_negation/2,
units_seaparated/4.
: mode
clausal_form(+, ),
clausal_form_of_negation(+, ),
pass_one(+, ),
pass_one(+, +, ),
pass_one(+, , +, +, ),
term_one(+, +, +, ),
term_one(+, +, +, +, ),
pass_two(+, ),
pass_two_pos(+, ),
pass_two_pos(+, , +, +),
term_two(+, , +),
term_var(+, +, ),
term_two(+, +, +, +),
pass_two_neg(+, , +, +),
sent_and(+, +, ),
sent_or(+, +, ),
units_separated(+, , , ),
contains(+, ?),
literally_contains(+, +),
does_not_literally_contain(+, ?).
: op(700, xfx, [contains,literally_contains,does_not_literally_contain]).
: op(910, fy, ~).
: op(920, xfy, and).
: op(930, xfy, or).
: op(940, xfx, [=>, <=>]).
units_separated([], [], [], []).
units_separated([clause([],[Neg])Clauses], PosL, [NegNegL], NonL) : !,
units_separated(Clauses, PosL, NegL, NonL).
units_separated([clause([Pos],[])Clauses], [PosPosL], NegL, NonL) : !,
units_separated(Clauses, PosL, NegL, NonL).
units_separated([ClauseClauses], PosL, NegL, [ClauseNonL]) :
units_separated(Clauses, PosL, NegL, NonL).
clausal_form(Formula, Clauses) :
pass_one(Formula, ClosedAndImplicationFree),
pass_two(ClosedAndImplicationFree, Clauses).
clausal_form_of_negation(Formula, Clauses) :
pass_one(Formula, ClosedAndImplicationFree),
pass_two(~ClosedAndImplicationFree, Clauses).
/*
The first pass over the formula does two things.
1a. It locates the free variables of the formula.
2. It applies the rules
A => B > B v ~A
A <=> B > (B v ~A) /\ (A v ~B)
if(A,B,C) > (B v ~A) /\ (A v C)
to eliminate implications. Even in a nonclausal
theorem prover this can be a good idea, eliminating
<=> and if is essential if each subformula is to
have a definite parity, and that in turn is vital
if we are going to replace existential quantifiers
by Skolem functions.
1b. It adds explicit quantifiers for the free variables.
The predicate which does all this is pass_one/5:
pass_one(+Formula, % The original formula
Translation, % its implicationfree equivalent
+Bound, % The binding environment
+Free0, % The variables known to be free
Free) % Free0 union Formula's free variables
The binding environment just tells us which variables occur in quantifiers
dominating this subformula, it doesn't matter yet whether they're
universal or existential.
The translated formula is still an , although there are practical
advantages to be gained by adopting a slightly different representation,
but the neatness of being able to say that
pass_one(F, G) > pass_one(G, G)
outweighs them.
*/
pass_one(Formula, ClosedAndImplicationFree) :
pass_one(Formula, ImplicationFree, [], [], FreeVariables),
pass_one(FreeVariables, ImplicationFree, ClosedAndImplicationFree).
pass_one([], Formula, Formula).
pass_one([VarVars], Formula, all(Var,Closure)) :
pass_one(Vars, Formula, Closure).
pass_one(all(Var,B), all(Var,D), Bound, Free0, Free) : !,
pass_one(B, D, [VarBound], Free0, Free).
pass_one(some(Var,B), some(Var,D), Bound, Free0, Free) : !,
pass_one(B, D, [VarBound], Free0, Free).
pass_one(A and B, C and D, Bound, Free0, Free) : !,
pass_one(A, C, Bound, Free0, Free1),
pass_one(B, D, Bound, Free1, Free).
pass_one(A or B, C or D, Bound, Free0, Free) : !,
pass_one(A, C, Bound, Free0, Free1),
pass_one(B, D, Bound, Free1, Free).
pass_one(A => B, D or ~C, Bound, Free0, Free) : !,
pass_one(A, C, Bound, Free0, Free1),
pass_one(B, D, Bound, Free1, Free).
pass_one(A <=> B, (D or ~C) and (C or ~D), Bound, Free0, Free) : !,
pass_one(A, C, Bound, Free0, Free1),
pass_one(B, D, Bound, Free1, Free).
pass_one(if(T,A,B), (C or ~U) and (D or U), Bound, Free0, Free) : !,
pass_one(T, U, Bound, Free0, Free1),
pass_one(A, C, Bound, Free1, Free2),
pass_one(B, D, Bound, Free2, Free).
pass_one(~A, ~C, Bound, Free0, Free) : !,
pass_one(A, C, Bound, Free0, Free).
pass_one(Atom, Atom, Bound, Free0, Free) :
% An Atom is "anything else". If Atoms were explicitly flagged,
% say by being written as +Atom, we wouldn't need those wretched
% cuts all over the place. The same is true of pass_two.
term_one(Atom, Bound, Free0, Free).
% term_one/4 scans a term which occurs in a context where some
% variables are Bound by quantifiers and some free variables (Free0)
% have already been discovered. Free is returned as the union of the
% free variables in this term with Free0. Note that though we call
% does_not_literally_contain twice, it is doing two different things.
% The first call determines that the variable is free. The second
% call is part of adding an element to a set, which could perhaps have
% been a binary tree or some other data structure.
term_one(Term, Bound, Free0, Free) :
nonvar(Term),
functor(Term, _, Arity),
!,
term_one(Arity, Term, Bound, Free0, Free).
term_one(Var, Bound, Free0, [VarFree0]) :
Bound does_not_literally_contain Var,
Free0 does_not_literally_contain Var,
!.
term_one(_, _, Free0, Free0).
term_one(0, _, _, Free0, Free0) : !.
term_one(N, Term, Bound, Free0, Free) :
arg(N, Term, Arg),
term_one(Arg, Bound, Free0, Free1),
M is N1, !,
term_one(M, Term, Bound, Free1, Free).
/*
pass_two does the following in one grand sweep:
1. The original formula might have used the same variable in any
number of quantifiers. In the output, each quantifier gets a
different variable.
2. But existentally quantified variables are replaced by new Skolem
functions, not by new variables. As a result, we can simply drop
all the quantifiers, every remaining variable is universally
quantified.
3. The rules
~ all(V, F) > some(V, ~F)
~ some(V, F) > all(V, ~F)
~ (A and B) > ~A or ~B
~ (A or B) > ~A and ~B
~ ~ A > A
are applied to move negations down in front of atoms.
4. The rules
A or A > A
A or ~A > true
A or true > true
A or false > A
(A or B) or C > A or (B or C)
(A and B) or C > (A or C) and (B or C)
A or (B and C) > (A or B) and (A or C)
A and true > A
A and false > false
(A and B) and C > A and (B and C)
are applied to the clauses which we build as we work our
way back up the tree. The rules
A and A > A
A and ~A > false
A and (~A or B) > A and B
are NOT applied. This is best done, if at all, after all the
clauses have been generated. The last two rules are special
cases of resolution, so it is doubtful whether it is worth
doing them at all.
The main predicate is pass_two_pos/4:
pass_two_pos(+Formula, % The formula to translate
Translation, % its translation
+Univ, % universal quantifiers in scope
+Rename) % how to rename variables
Rename is var  var(Old,New,Rename), where Old is a source variable,
and New is either a new variable (for universal quantifiers) or a
Skolem function applied to the preceding new variables (for existential
quantifiers). Univ is those New elements of the Rename argument which
are variables. pass_two_neg produces the translation of its Formula's
*negation*, this saves building the negation and then handling it.
*/
pass_two(ClosedAndImplicationFree, ClausalForm) :
pass_two_pos(ClosedAndImplicationFree, PreClausalForm, [], var),
pass_two_pos(PreClausalForm, ClausalForm).
% pass_two_pos/2 does two things. First, if there was only one clause,
% pass_two_pos/4 wouldn't have wrapped it up in a list. This we do here.
% Second, if one of the clauses is "false", we return that as the only
% clause. This would be the place to apply A & A > A.
pass_two_pos(clause(P,N), [clause(P,N)]) : !.
pass_two_pos(Sentence, [clause([],[])]) :
Sentence contains clause([],[]),
!.
pass_two_pos(Sentence, Sentence).
pass_two_pos(all(Var,B), Translation, Univ, Rename) : !,
pass_two_pos(B, Translation, [NewUniv], var(Var,New,Rename)).
pass_two_pos(some(Var,B), Translation, Univ, Rename) : !,
gensym('f', SkolemFunction),
SkolemTerm =.. [SkolemFunctionUniv],
pass_two_pos(B, Translation, Univ, var(Var,SkolemTerm,Rename)).
pass_two_pos(A and B, Translation, Univ, Rename) : !,
pass_two_pos(A, C, Univ, Rename),
pass_two_pos(B, D, Univ, Rename),
sent_and(C, D, Translation).
pass_two_pos(A or B, Translation, Univ, Rename) : !,
pass_two_pos(A, C, Univ, Rename),
pass_two_pos(B, D, Univ, Rename),
sent_or(C, D, Translation).
pass_two_pos(~A, Translation, Univ, Rename) : !,
pass_two_neg(A, Translation, Univ, Rename).
pass_two_pos(true, [], _, _) : !.
pass_two_pos(false, clause([],[]), _, _) : !.
pass_two_pos(Atom, clause([Renamed],[]), _, Rename) :
% An Atom is "anything else", hence the cuts above.
term_two(Atom, Renamed, Rename).
pass_two_neg(all(Var,B), Translation, Univ, Rename) : !,
gensym('g', SkolemFunction),
SkolemTerm =.. [SkolemFunctionUniv],
pass_two_neg(B, Translation, Univ, var(Var,SkolemTerm,Rename)).
pass_two_neg(some(Var,B), Translation, Univ, Rename) : !,
pass_two_neg(B, Translation, [NewUniv], var(Var,New,Rename)).
pass_two_neg(A and B, Translation, Univ, Rename) : !,
pass_two_neg(A, C, Univ, Rename),
pass_two_neg(B, D, Univ, Rename),
sent_or(C, D, Translation).
pass_two_neg(A or B, Translation, Univ, Rename) : !,
pass_two_neg(A, C, Univ, Rename),
pass_two_neg(B, D, Univ, Rename),
sent_and(C, D, Translation).
pass_two_neg(~A, Translation, Univ, Rename) : !,
pass_two_pos(A, Translation, Univ, Rename).
pass_two_neg(true, clause([],[]), _, _) : !.
pass_two_neg(false, [], _, _) : !.
pass_two_neg(Atom, clause([],[Renamed]), _, Rename) :
% An Atom is "anything else", hence the cuts above.
term_two(Atom, Renamed, Rename).
term_two(OldTerm, NewTerm, Rename) :
nonvar(OldTerm),
functor(OldTerm, FunctionSymbol, Arity),
functor(NewTerm, FunctionSymbol, Arity),
!,
term_two(Arity, OldTerm, NewTerm, Rename).
term_two(OldVar, NewTerm, Rename) :
term_var(Rename, OldVar, NewTerm).
term_var(var(Old,New,_), Var, New) :
Old == Var,
!.
term_var(var(_,_,Rest), Var, New) :
term_var(Rest, Var, New).
term_two(0, _, _, _) : !.
term_two(N, OldTerm, NewTerm, Rename) :
arg(N, OldTerm, OldArg),
term_two(OldArg, NewArg, Rename),
arg(N, NewTerm, NewArg),
M is N1, !,
term_two(M, OldTerm, NewTerm, Rename).
/*
sent_and(S1, S2, "S1 and S2")
sent_or(S1, S2, "S1 or S2")
perform the indicated logical operations on clauses or sets of
clauses (sentences), using a fair bit of propositional reasoning
(hence our use of "literally" to avoid binding variables) to try
to keep the results simple. There are several rules concerning
conjunction which are *not* applied, but even checking for
A and A > A
would require us to recognise alphabetic variants of A rather
than literal identity. So far the naivety abount conjunction
has not proved to be a practical problem.
*/
sent_or(clause(P1,_), clause(_,N2), []) :
P1 contains Atom,
N2 literally_contains Atom,
!.
sent_or(clause(_,N1), clause(P2,_), []) :
N1 contains Atom,
P2 literally_contains Atom,
!.
sent_or(clause(P1,N1), clause(P2,N2), clause(P3,N3)) : !,
ord_union(P1, P2, P3),
ord_union(N1, N2, N3).
sent_or([], _, []) : !.
sent_or(_, [], []) : !.
sent_or([ClauseClauses], Sentence, Answer) : !,
sent_or(Sentence, Clause, X),
sent_or(Clauses, Sentence, Y),
sent_and(X, Y, Answer).
sent_or(Sentence, [ClauseClauses], Answer) : !,
sent_or(Sentence, Clause, X),
sent_or(Clauses, Sentence, Y),
sent_and(X, Y, Answer).
sent_and([], Sentence, Sentence) : !.
sent_and(Sentence, [], Sentence) : !.
sent_and([H1T1], [H2T2], [H1,H2T3]) : !,
sent_and(T1, T2, T3).
sent_and([H1T1], Clause, [Clause,H1T1]) : !.
sent_and(Clause, [H2T2], [Clause,H2T2]) : !.
sent_and(Clause1, Clause2, [Clause1,Clause2]).
[Head_] contains Head.
[_Tail] contains Something :
Tail contains Something.
[Head_] literally_contains Something :
Head == Something,
!.
[_Tail] literally_contains Something :
Tail literally_contains Something.
[] does_not_literally_contain Anything.
[HeadTail] does_not_literally_contain Something :
Head \== Something,
Tail does_not_literally_contain Something.
/*
Debugging kit.
portray_sentence(ListOfClauses)
displays a list of clauses, one per line.
portray_clause(Clause)
displays a single clause in "Kowalski notation"
t(Formula)
translates a formula and prints the result.
: public
t1/0,t9/0,t/1.
portray_sentence([Clause]) : !,
portray_clause(Clause),
nl.
portray_sentence([ClauseClauses]) :
portray_clause(Clause),
write(' AND'), nl,
portray_sentence(Clauses).
portray_sentence([]) :
write('TRUE'), nl.
portray_clause(clause(PosAtoms, NegAtoms)) :
numbervars(PosAtoms, 0, N),
numbervars(NegAtoms, N, _),
portray_clause(PosAtoms, ' v '),
write(' < '),
portray_clause(NegAtoms, ' & '),
fail.
portray_clause(_).
portray_clause([Atom], _) : !,
print(Atom).
portray_clause([AtomAtoms], Separator) :
print(Atom), write(Separator),
portray_clause(Atoms, Separator).
portray_clause([], _) :
write([]).
t(X) :
clausal_form(X, Y),
portray_sentence(Y).
t1 : t((a=>b) and (b=>c) and (c=>d) and (d=>a) => (a<=>d)).
t2 : t(continuous(F,X) <=> all(Epsilon, Epsilon > 0 =>
some(Delta, Delta > 0 and all(Y,
abs(YX) < Delta => abs(val(F,Y)val(F,X)) < Epsilon
)))).
t3 : clausal_form_of_negation(
( subset(S1,S2) <=> all(X, member(X,S1) => member(X,S2) )) =>
( subset(T1,T2) and subset(T2,T3) => subset(T1,T3) ) ,Y),
portray_sentence(Y).
t4 : t(subset(T1,T2) and subset(T2,T3) => subset(T1,T3)).
t5 : t((a=>b) and (b=>c)).
t6 : t(~(a and b)).
t7 : t((a and b) or c).
t8 : t((a and b) or (a and ~b) or (~a and b) or (~a and ~b)).
t9 : t(
(true(P) <=> t(w0,P)) and
(t(W1,P1 and P2) <=> t(W1,P1) and t(W1,P2)) and
(t(W1,P1 or P2) <=> t(W1,P1) or t(W1,P2)) and
(t(W1,P1 => P2) <=> (t(W1,P1) => t(W1,P2))) and
(t(W1,P1 <=> P2) <=> (t(W1,P1) <=> t(W1,P2))) and
(t(W1,~P1) <=> ~t(W1,P1)) and
(t(W1,know(A1,P1)) <=> all(W2,k(A1,W1,W2)=>t(W2,P1))) and
k(A1,W1,W1) and
(k(A1,W1,W2) => (k(A1,W2,W3) => k(A1,W1,W3))) and
(k(A1,W1,W2) => (k(A1,W1,W3) => k(A1,W2,W3))) and
(t(W1,know(A,P)) <=> all(W2,k(A,W1,W2) => t(W2,P)))
).
*/