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/*%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 16 17\chapter 18[Die Datei {\tt tom\_negation\_normal\_form}] 19{Die Datei {\Huge \tt tom\_negation\_normal\_form}} 20 21\Predicate negation_normal_form/2(+Formula, -NormalizedFormula). 22 23The transformation of a formula to its negation normal form. This one 24is the top level predicate for the one to follow. The transformation can 25be described by a function which we will call {\em nnf}. 26 27\[ nnf(\varphi) = nnf(\varphi,0) \] 28 29\PL*/ 30 31negation_normal_form(Formula, NormalizedFormula):- 32 negation_normal_form(Formula, 0, NormalizedFormula). 33 34/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 35 36\Predicate negation_normal_form/3(+Formula, ?Polarity, -NormalizedFormula). 37 38As the translation assumes a formula in its negation normalform, 39we have to transform the formula before translating it. This has been 40done in a rather conventional way, analysing the formula structure and 41eventually changing the operators to their duals, according to the polarity. 42The function {\em nnf} will specify the behaviour. 43 44\PL*/ 45 46/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 47 48\[ nnf(\varphi \leftrightarrow \psi,P) = \left\{ \begin{array}{ll} nnf(\varphi \to \psi,0) \wedge nnf(\psi \to \varphi,0) & \mbox{ if \(P 49= 0\)}\\ nnf(\varphi \to \psi,1) \vee nnf(\psi \to \varphi, 1)& \mbox{ otherwise} \end{array} \right. \] 50 51The corresponding logical equivalences are: 52\begin{eqnarray*} 53 \varphi \leftrightarrow \psi & = & (\varphi \to \psi) \wedge (\psi \to \varphi) \\ 54 \neg(\varphi \leftrightarrow \psi) & = & \neg(\varphi \to \psi) \vee \neg(\psi \to \varphi) 55\end{eqnarray*} 56 57\PL*/ 58 59negation_normal_form( equivalent(Form1, Form2), 0, 60 and(NormForm1, NormForm2)):- 61 !, 62 negation_normal_form(implies(Form1, Form2), 0, NormForm1), 63 negation_normal_form(implies(Form2, Form1), 0, NormForm2). 64 65negation_normal_form( equivalent(Form1, Form2), 1, 66 or(NormForm1, NormForm2)):- 67 !, 68 negation_normal_form(implies(Form1, Form2), 1, NormForm1), 69 negation_normal_form(implies(Form2, Form1), 1, NormForm2). 70 71/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 72 73\[ nnf(\varphi \to \psi,P) = \left\{ \begin{array}{ll} nnf(\neg \varphi,0) \vee nnf(\psi,0) & \mbox{ if \(P 74= 0\)}\\ nnf(\varphi,0) \wedge nnf(\neg\psi, 0)& \mbox{ otherwise} \end{array} \right. \] 75 76The corresponding logical equivalences are: 77\begin{eqnarray*} 78 \varphi \to \psi & = & \neg \varphi \vee \psi\\ 79 \neg(\varphi \to \psi) & = & \varphi \wedge \neg \psi 80\end{eqnarray*} 81 82\PL*/ 83 84negation_normal_form( implies(Formula1, Formula2), 0, 85 or(NormalFormula1,NormalFormula2)):- 86 !, 87 negation_normal_form(not(Formula1), 0, NormalFormula1), 88 negation_normal_form(Formula2, 0, NormalFormula2). 89 90negation_normal_form( implies(Formula1, Formula2), 1, 91 and(NormalFormula1,NormalFormula2)):- 92 !, 93 negation_normal_form(Formula1, 0, NormalFormula1), 94 negation_normal_form(not(Formula2), 0, NormalFormula2). 95 96/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 97 98\[ nnf(\varphi \wedge \psi,P) = \left\{ \begin{array}{ll} nnf(\varphi,0) \wedge nnf(\psi,0) & \mbox{ if \(P 99= 0\)}\\ nnf(\neg \varphi,0) \vee nnf(\neg\psi, 0)& \mbox{ otherwise} \end{array} \right. \] 100 101The corresponding logical equivalence is one of de Morgan's laws: 102\begin{eqnarray*} 103 \neg(\varphi \wedge \psi) & = & \neg \varphi \vee \neg \psi 104\end{eqnarray*} 105 106\PL*/ 107 108negation_normal_form( and(Formula1, Formula2), 0, 109 and(NormalFormula1, NormalFormula2)):- 110 !, 111 negation_normal_form(Formula1, 0, NormalFormula1), 112 negation_normal_form(Formula2, 0, NormalFormula2). 113 114negation_normal_form( and(Formula1, Formula2), 1, 115 or(NormalFormula1, NormalFormula2)):- 116 !, 117 negation_normal_form(not(Formula1), 0, NormalFormula1), 118 negation_normal_form(not(Formula2), 0, NormalFormula2). 119 120/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 121 122\[ nnf(\varphi \vee \psi,P) = \left\{ \begin{array}{ll} nnf(\varphi,0) \vee nnf(\psi,0) & \mbox{ if \(P 123= 0\)}\\ nnf(\neg \varphi,0) \wedge nnf(\neg\psi, 0)& \mbox{ otherwise} \end{array} \right. \] 124 125The corresponding logical equivalence is one of de Morgan's laws: 126\begin{eqnarray*} 127 \neg(\varphi \vee \psi) & = & \neg \varphi \wedge \neg \psi 128\end{eqnarray*} 129 130\PL*/ 131 132negation_normal_form( or(Formula1, Formula2), 0, 133 or(NormalFormula1, NormalFormula2)):- 134 !, 135 negation_normal_form(Formula1, 0, NormalFormula1), 136 negation_normal_form(Formula2, 0, NormalFormula2). 137 138negation_normal_form( or(Formula1, Formula2), 1, 139 and(NormalFormula1, NormalFormula2)):- 140 !, 141 negation_normal_form(not(Formula1), 0, NormalFormula1), 142 negation_normal_form(not(Formula2), 0, NormalFormula2). 143 144/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 145 146\[ nnf(\neg \varphi,P) = \left\{ \begin{array}{ll} nnf(\varphi',0) & \mbox{ if \(\varphi = \neg \varphi'\)}\\ nnf(\varphi,(P + 1) \bmod 2) & \mbox{ otherwise} \end{array} \right. \] 147 148\PL*/ 149 150negation_normal_form( not(Formula1), Polarity, NormalFormula):- 151 !, 152 ( Formula1 = not(NewFormula) -> 153 negation_normal_form(NewFormula, Polarity, NormalFormula) 154 ; NewPolarity is (Polarity + 1) mod 2, 155 negation_normal_form(Formula1, NewPolarity, NormalFormula) 156 ). 157 158/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 159 160\[ nnf(\forall X \: \varphi,P) = \left\{ \begin{array}{ll} \forall X \: nnf(\varphi,0) & \mbox{ if \(P = 0\)}\\ \exists X \: nnf(\varphi,1) & \mbox{ otherwise} \end{array} \right. \] 161 162The corresponding logical equivalence is the duality of the quantifiers: 163\[ \neg \forall X \: \varphi = \exists X \: \neg \varphi \] 164 165\PL*/ 166 167negation_normal_form(forall(:(Var, Formula1)), 0 , 168 forall(:(Var, NewFormula1))):- 169 !, 170 negation_normal_form(Formula1, 0, NewFormula1). 171 172negation_normal_form(forall(:(Var, Formula1)), 1 , 173 exists(:(Var, NewFormula1))):- 174 !, 175 negation_normal_form(Formula1, 1, NewFormula1). 176 177/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 178 179\[ nnf(\exists X \: \varphi,P) = \left\{ \begin{array}{ll} \exists X \: nnf(\varphi,0) & \mbox{ if \(P = 0\)}\\ \forall X \: nnf(\varphi,1) & \mbox{ otherwise} \end{array} \right. \] 180 181Again, the duality of the quantifiers is applied. 182 183\PL*/ 184 185negation_normal_form(exists(:(Var, Formula1)), 0 , 186 exists(:(Var, NewFormula1))):- 187 !, 188 negation_normal_form(Formula1, 0, NewFormula1). 189 190negation_normal_form(exists(:(Var, Formula1)), 1 , 191 forall(:(Var, NewFormula1))):- 192 !, 193 negation_normal_form(Formula1, 1, NewFormula1). 194 195/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 196 197\[ nnf(\Box_a \: \varphi,P) = \left\{ \begin{array}{ll} \Box_a\: nnf(\varphi,0) & \mbox{ if \(P = 0\)}\\ \Diamond_a\: nnf(\varphi,1) & \mbox{ otherwise} \end{array} \right. \] 198 199The corresponding logical equivalence is the duality of the modal operators: 200\[ \neg \Box X \: \varphi = \Diamond X \: \neg \varphi \] 201 202\PL*/ 203 204negation_normal_form(box(:(Sort,Formula1)), 0, 205 box(:(Sort,NewFormula1))):- 206 !, 207 negation_normal_form(Formula1, 0, NewFormula1). 208 209negation_normal_form(box(:(Sort,Formula1)), 1, 210 diamond(:(Sort,NewFormula1))):- 211 !, 212 negation_normal_form(Formula1, 1, NewFormula1). 213 214negation_normal_form(box(Formula1), 0, box(NewFormula1)):- 215 !, 216 negation_normal_form(Formula1, 0, NewFormula1). 217 218negation_normal_form(box(Formula1), 1, diamond(NewFormula1)):- 219 !, 220 negation_normal_form(Formula1, 1, NewFormula1). 221 222/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 223 224\[ nnf(\Diamond_a \: \varphi,P) = \left\{ \begin{array}{ll} \Diamond_a \: nnf(\varphi,0) & \mbox{ if \(P = 0\)}\\ \Box_a\: nnf(\varphi,1) & \mbox{ otherwise} \end{array} \right. \] 225 226Again, the duality of the modal operators is used. 227 228\PL*/ 229 230negation_normal_form(diamond(:(Sort,Formula1)), 0, 231 diamond(:(Sort,NewFormula1))):- 232 !, 233 negation_normal_form(Formula1, 0, NewFormula1). 234 235negation_normal_form(diamond(:(Sort,Formula1)), 1, 236 box(:(Sort,NewFormula1))):- 237 !, 238 negation_normal_form(Formula1, 1, NewFormula1). 239 240negation_normal_form(diamond(Formula1), 0, diamond(NewFormula1)):- 241 !, 242 negation_normal_form(Formula1, 0, NewFormula1). 243 244negation_normal_form(diamond(Formula1), 1, box(NewFormula1)):- 245 !, 246 negation_normal_form(Formula1, 1, NewFormula1). 247 248/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 249 250If none of the above cases applies, we use the following clause: 251\[ nnf(\varphi,P) = \left\{ \begin{array}{ll} \varphi & \mbox{ if \(P = 0\)}\\ \neg \varphi & \mbox{ otherwise} \end{array} \right. \] 252This is because apparently we are at the literal level. 253 254\PL*/ 255 256negation_normal_form(Formula, Polarity, NormalFormula):- 257 ( Polarity = 0 -> 258 NormalFormula = Formula 259 ; NormalFormula = not(Formula) 260 ). 261/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 262\EndProlog */