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). 32info(filter,"$Revision: 1.0 $","normal form filter").
38:- lib(op_def). 48nnf(Stream,OutStream) :-
49 repeat,
50 read(Stream,Term),
51 ( Term = end_of_file ->
52 true
53 ; writeclause(OutStream,Term),
54 fail
55 ),
56 !.
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 ).