La semantica della formula `(A ∨ C)` nel mondo `v20` in cui
`A` vale `2` e `C` vale `0` deve valere `1`.
+ Decommenta ed esegui.
*)
-eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20.
+
+(* eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20. *)
(*DOCBEGIN
Testare la funzione `negate`. Il risultato atteso è:
- FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1)))
+ FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1)))
+
+ Decommenta ed esegui
*)
-eval normalize on (negate (FOr (FAtom 0) (FImpl FTop (FAtom 1)))).
+(* eval normalize on (negate (FOr (FAtom 0) (FImpl FTop (FAtom 1)))). *)
(* ATTENZIONE
==========
Testare la funzione `dualize`. Il risultato atteso è:
FAnd (FNot (FAtom O)) (FOr (FAtom 1) FTop)
+
+ Decommenta ed esegui.
*)
-eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))).
+(* eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))). *)
(* Spiegazione
===========