1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%% $Id: nnf.pl,v 1.5 1995/01/27 13:45:38 gerd Exp $
    3%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    4%%% 
    5%%% This file is part of ProCom.
    6%%% It is distributed under the GNU General Public License.
    7%%% See the file COPYING for details.
    8%%% 
    9%%% (c) Copyright 1995 Gerd Neugebauer
   10%%% 
   11%%% Net: gerd@imn.th-leipzig.de
   12%%% 
   13%%%****************************************************************************
   14
   15:- module_interface(nnf). /*%-------------------------------------------------
   16\FileId{Gerd Neugebauer}{\RCSstrip$Revision: 1.5 $}
   17
   18The filter {\tt nnf} is a filter which produces the negation normal form
   19of a formula. The usual de Morgan laws are applied, includeing those for
   20quantifiers and modalities.
   21
   22\PL*/
   23:- export nnf/2,
   24          make_nnf/3.
   25
   26:- begin_module(nnf).   27/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   28
   29Our identification as a filter for \ProTop.
   30
   31\PL*/
   32info(filter,"$Revision: 1.0 $","normal form filter").
   33/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   34
   35We need some definitions from the system.
   36
   37\PL*/
   38:-	lib(op_def).   39/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   40
   41\Predicate nnf/2(+Stream, +OutStream).
   42
   43This is an empty filter. No action is performed except that terms are
   44transferred from the input stream |Stream| to the output stream
   45|OutStream|.
   46
   47\PL*/
   48nnf(Stream,OutStream) :-
   49	repeat,
   50	read(Stream,Term),
   51	( Term = end_of_file ->
   52	    true
   53	;   writeclause(OutStream,Term),
   54	    fail
   55	),
   56	!.
   57/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   58
   59\Predicate make_nnf/3(+Formula, ?Polarity, -NormalizedFormula).
   60
   61As the translation assumes a formula in its negation normalform,
   62we have to transform the formula before translating it. This has been
   63done in a rather conventional way, analysing the formula structure and
   64eventually changing the operators to their duals, according to the polarity.
   65
   66\PL*/
   67make_nnf(Formula,Polarity,NormalFormula):-
   68	var(Formula),
   69	!,
   70	( Polarity = 0 ->
   71	    NormalFormula = Formula
   72	; Polarity = 1 ->
   73	    NormalFormula =.. [not, Formula]
   74	).
   75
   76make_nnf( equivalent(Form1, Form2), 0, and(NormForm1, NormForm2)):-
   77	!,
   78	make_nnf(implies(Form1, Form2), 0, NormForm1),
   79	make_nnf(implies(Form2, Form1), 0, NormForm2).
   80
   81make_nnf( equivalent(Form1, Form2), 1, or(NormForm1, NormForm2)):-
   82	!,
   83	make_nnf(implies(Form1, Form2), 1, NormForm1),
   84	make_nnf(implies(Form2, Form1), 1, NormForm2).
   85
   86make_nnf( implies(Formula1, Formula2), 0, or(NormalFormula1,NormalFormula2)):-
   87	!,
   88	make_nnf(not Formula1, 0, NormalFormula1),
   89	make_nnf(Formula2, 0, NormalFormula2).
   90
   91make_nnf( implies(Formula1, Formula2), 1, and(NormalFormula1,NormalFormula2)):-
   92	!,
   93	make_nnf(Formula1, 0, NormalFormula1),
   94	make_nnf(not Formula2, 0, NormalFormula2).
   95
   96make_nnf( and(Formula1, Formula2), 0, and(NormalFormula1, NormalFormula2)):-
   97	!,
   98	make_nnf(Formula1, 0, NormalFormula1),
   99	make_nnf(Formula2, 0, NormalFormula2).
  100
  101make_nnf( and(Formula1, Formula2), 1, or(NormalFormula1, NormalFormula2)):-
  102	!,
  103	make_nnf(not Formula1, 0, NormalFormula1),
  104	make_nnf(not Formula2, 0, NormalFormula2).
  105
  106make_nnf( or(Formula1, Formula2), 0, or(NormalFormula1, NormalFormula2)):-
  107	!,
  108	make_nnf(Formula1, 0, NormalFormula1),
  109	make_nnf(Formula2, 0, NormalFormula2).
  110
  111make_nnf( or(Formula1, Formula2), 1, and(NormalFormula1, NormalFormula2)):-
  112	!,
  113	make_nnf(not Formula1, 0, NormalFormula1),
  114	make_nnf(not Formula2, 0, NormalFormula2).
  115
  116make_nnf( not(Formula1), Polarity, NormalFormula):-
  117	!,
  118	( Formula1 =.. [not, NewFormula] ->
  119	    make_nnf(NewFormula, Polarity, NormalFormula)
  120	; NewPolarity is (Polarity + 1) mod 2,
  121	    make_nnf(Formula1, NewPolarity, NormalFormula)
  122	).
  123
  124make_nnf(forall(:(Var, Formula1)), 0 , forall(:(Var, NewFormula1))):-
  125	!,
  126	make_nnf(Formula1, 0, NewFormula1).
  127
  128make_nnf(forall(:(Var, Formula1)), 1 , exists(:(Var, NewFormula1))):-
  129	!,
  130	make_nnf(Formula1, 1, NewFormula1).
  131
  132make_nnf(exists(:(Var, Formula1)), 0 , exists(:(Var, NewFormula1))):-
  133	!,
  134	make_nnf(Formula1, 0, NewFormula1).
  135
  136make_nnf(exists(:(Var, Formula1)), 1 , forall(:(Var, NewFormula1))):-
  137	!,
  138	make_nnf(Formula1, 1, NewFormula1).
  139
  140make_nnf(box(:(Sort,Formula1)), 0, box(:(Sort,NewFormula1))):-
  141	!,
  142	make_nnf(Formula1, 0, NewFormula1).
  143
  144make_nnf(box(:(Sort,Formula1)), 1, diamond(:(Sort,NewFormula1))):-
  145	!,
  146	make_nnf(Formula1, 1, NewFormula1).
  147
  148make_nnf(box(Formula1), 0, box(NewFormula1)):-
  149	!,
  150	make_nnf(Formula1, 0, NewFormula1).
  151
  152make_nnf(box(Formula1), 1, diamond(NewFormula1)):-
  153	!,
  154	make_nnf(Formula1, 1, NewFormula1).
  155
  156make_nnf(diamond(:(Sort,Formula1)), 0, diamond(:(Sort,NewFormula1))):-
  157	!,
  158	make_nnf(Formula1, 0, NewFormula1).
  159
  160make_nnf(diamond(:(Sort,Formula1)), 1, box(:(Sort,NewFormula1))):-
  161	!,
  162	make_nnf(Formula1, 1, NewFormula1).
  163
  164make_nnf(diamond(Formula1), 0, diamond(NewFormula1)):-
  165	!,
  166	make_nnf(Formula1, 0, NewFormula1).
  167
  168make_nnf(diamond(Formula1), 1, box(NewFormula1)):-
  169	!,
  170	make_nnf(Formula1, 1, NewFormula1).
  171
  172make_nnf(Formula, Polarity, NormalFormula):-
  173	( Polarity = 0 ->
  174	    NormalFormula = Formula
  175	; Polarity = 1 ->
  176	    NormalFormula =.. [not, Formula]
  177	).
  178/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  179\EndProlog */