/* --- Copyright University of Sussex 1989. All rights reserved. ----------
 > File:            $poplocal/local/plog/lib/normalize.pl
 > Purpose:         Normalize logical expressions
 > Author:          Harry Barrow, Feb  1 1989
 > Documentation:   TEACH * NORMALIZE
 > Related Files:   SHOWLIB * CHECKER, TEACH * CHECKER
 */

/*
> NORMALIZE.PL is a rewriting system to put logical expressions (in
> convenient notation) into clausal form.  Logical variables, represented
> by Prolog variables, can only be universally quantified over entire
> expression; existential quantification is not allowed.
> I.e.  <expr involving X,Y,Z> is assumed to mean  For all X,Y,Z <expr>
>
> Note that rewriting is only done on the logical connectives, which means
> that prolog variables are safe if they are wrapped up inside predicate
> terms.
>
> There are two top-level procedures:
>
>       normalize(Expression,NewExpression).
>
>   which rewrites a logical expression (Expression) to produce a new
>   version in a standard form (NewExpression), determined by a set
>   of rewriting rules (normalize_rule).
>
>       clausify(Expression,Clauses).
>
>   which rewrites a logical expression (Expression) to produce an
>   internal representation for resolution theorem proving.  The
>   result (Clauses) is a list (representing a conjunction) of clauses,
>   each clause being itself a list (representing a disjunction) of
>   Prolog terms (representing literals).  A negative literal is
>   represented as -(Term).
>
*/

/* Logical operator declarations.
*/

:- op(70, fy,'not').       % NOT
:- op(80,xfy,'and').       % AND
:- op(80,xfy,'&').         % AND (alternative)
:- op(85,xfy,'or').        % OR
:- op(85,xfy,'#').         % OR  (alternative)
:- op(85,xfy,'xor').       % EXCLUSIVE OR
:- op(90,xfy,'=>').        % IMPLIES
:- op(90,xfy,'<=').        % IMPLIED BY
:- op(90,xfy,'<=>').       % EQUIVALENT


/* Convert a logical expression to internal form.
    result is a list representing a conjunction (and)
    of lists representing disjunctions (ors).
*/
clausify(Form,Clauses) :-
    normalize(Form,NForm),
    clause_and(NForm,Clauses).


clause_and(X and YS, [CX|CYS]) :- !,
    clause_or(X,CX),
    clause_and(YS,CYS).
clause_and(X,[CX]) :-
    clause_or(X,CX).

clause_or((X or YS),[CX|CYS]) :- !,
    clause_not(X,CX),
    clause_or(YS,CYS).
clause_or(X,[CX]) :-
    clause_not(X,CX).

clause_not(not(X),-(X)) :- !.
clause_not(X,X).


/* Procedure to rewrite expressions according to rules
*/
normalize(Expr,NExpr) :-
    normalize(Expr,NExpr,10000).

normalize(Expr,Expr,Depth) :-
    Depth < 1, !.                               % Depth limit -- Do nothing
normalize(Expr,NewExpr,Depth) :-
    functor(Expr,Fn,NArgs),
    normalizable(Fn,NArgs), !,                  % Normalizable
    functor(NExpr,Fn,NArgs),                    % Build a new skeleton term
    Depth1 is Depth-1,
    normalize_args(NArgs,Expr,NExpr,Depth1),    % Normalize arguments
    normalize_once(NExpr,NExpr1,NDepth),        % Normalize result -> New Depth
    normalize(NExpr1,NewExpr,NDepth).           % Iterate
normalize(Expr,Expr,Depth).                     % Can't normalize -- Leave alone


normalize_args(0,Expr,NExpr,Depth) :- !.        % Done
normalize_args(NArgs,Expr,NExpr,Depth) :-
    arg(NArgs,Expr,Arg),
    normalize(Arg,NArg,Depth),
    arg(NArgs,NExpr,NArg),
    NArgs1 is NArgs -1,
    normalize_args(NArgs1,Expr,NExpr,Depth).


normalize_once(Expr,NExpr,NDepth) :-
    normalize_rule(Expr,NExpr,NDepth), !.
normalize_once(Expr,Expr,0).


/* Rewriting rules for functions that can be normalized
*/

normalizable((not),1).
normalizable((-),1).
normalizable((+),1).
normalizable((and),2).
normalizable((&),2).
normalizable((or),2).
normalizable((#),2).
normalizable((xor),2).
normalizable((=>),2).
normalizable((<=),2).
normalizable((<=>),2).
normalizable((.),2).


/* Basic rewriting rules to put into clausal form.
    Each rule has a pattern to match, a pattern to replace it with,
    and a depth to specify how much rewriting the result may need.
*/

normalize_rule( +(X), X, 0).                            % standardise
normalize_rule( -(X), not(X), 0).                       %   notation
normalize_rule( (X & Y), (X and Y), 1).
normalize_rule( (X # Y), (X or Y), 1).


normalize_rule(not(true),false,0).                      % negation
normalize_rule(not(false),true,0).

normalize_rule(not(not(X)),X,0).                        % double negation

normalize_rule((X and true),X,0).                       % simplify and
normalize_rule((true and X),X,0).
normalize_rule((_X and false),false,0).
normalize_rule((false and _X),false,0).
normalize_rule((not X and X),false,0).
normalize_rule((X and not X),false,0).

normalize_rule((_X or true),true,0).                    % simplify or
normalize_rule((true or _X),true,0).
normalize_rule((X or false),X,0).
normalize_rule((false or X),X,0).
normalize_rule((not X or X),true,0).
normalize_rule((X or not X),true,0).

normalize_rule(((X and Y) and Z),(X and Y and Z),2).    % nest on the right
normalize_rule(((X or Y) or Z),(X or Y or Z),2).

normalize_rule(not(X and Y),(not(X) or not(Y)),2).      % De Morgan's laws
normalize_rule(not((X or Y)),(not(X) and not(Y)),2).

normalize_rule(((X and Y) or Z), ((X or Z) and (Y or Z)),2).   % Distribution
normalize_rule((X or (Y and Z)), ((X or Y) and (X or Z)),2).

normalize_rule((X xor Y),(X and not Y) or (not X and Y),3). % Expand xor

normalize_rule((X => Y),( not(X) or Y),2).              % Expand implications
normalize_rule((Y <= X),( not(X) or Y),2).
normalize_rule((X <=> Y), ((X => Y) and (Y => X)),2).

normalize_rule([X],X,0).                              % Clause to disjunction
normalize_rule([X|L],(X or L),2).

/* --- Revision History ---------------------------------------------------
--- Harry Barrow, Feb  1 1989  Initial installation in library
 */
