1(* ========================================================================= *) 2(* DEFINITIONAL CNF IN HOL. *) 3(* Created by Joe Hurd, February 2002. *) 4(* ========================================================================= *) 5 6signature defCNF = 7sig 8 9include Abbrev 10 11(* ------------------------------------------------------------------------- *) 12(* Definitional Negation Normal Form *) 13(* *) 14(* Example: *) 15(* (~(p = ~(q = r)) = ~(~(p = q) = r)) *) 16(* = *) 17(* ((p = (q = r)) = ((p = ~q) = ~r)) *) 18(* ------------------------------------------------------------------------- *) 19 20val DEF_NNF_CONV : conv 21 22(* ------------------------------------------------------------------------- *) 23(* Definitional Conjunctive Normal Form *) 24(* *) 25(* Example: *) 26(* (~(p = ~(q = r)) = ~(~(p = q) = r)) *) 27(* = *) 28(* ?v v1 v2 v3 v4. *) 29(* (v4 \/ v1 \/ v3) /\ (v4 \/ ~v1 \/ ~v3) /\ (v1 \/ ~v3 \/ ~v4) /\ *) 30(* (v3 \/ ~v1 \/ ~v4) /\ (v3 \/ v2 \/ ~r) /\ (v3 \/ ~v2 \/ r) /\ *) 31(* (v2 \/ r \/ ~v3) /\ (~r \/ ~v2 \/ ~v3) /\ (v2 \/ p \/ ~q) /\ *) 32(* (v2 \/ ~p \/ q) /\ (p \/ q \/ ~v2) /\ (~q \/ ~p \/ ~v2) /\ *) 33(* (v1 \/ p \/ v) /\ (v1 \/ ~p \/ ~v) /\ (p \/ ~v \/ ~v1) /\ *) 34(* (v \/ ~p \/ ~v1) /\ (v \/ q \/ r) /\ (v \/ ~q \/ ~r) /\ *) 35(* (q \/ ~r \/ ~v) /\ (r \/ ~q \/ ~v) /\ v4 *) 36(* ------------------------------------------------------------------------- *) 37 38val PURE_DEF_CNF_CONV : conv (* Introduces definitions *) 39val CLEANUP_DEF_CNF_CONV : conv (* Converts defns to CNF *) 40val DEF_CNF_CONV : conv (* NNF + PURE + CLEANUP *) 41 42(* ------------------------------------------------------------------------- *) 43(* Definitional Conjunctive Normal Form using variable vectors *) 44(* *) 45(* Example: *) 46(* (~(p = ~(q = r)) = ~(~(p = q) = r)) *) 47(* = *) 48(* ?v. *) 49(* (v 4 \/ v 1 \/ v 3) /\ (v 4 \/ ~v 1 \/ ~v 3) /\ *) 50(* (v 1 \/ ~v 3 \/ ~v 4) /\ (v 3 \/ ~v 1 \/ ~v 4) /\ *) 51(* (~r \/ ~v 2 \/ ~v 3) /\ (v 2 \/ r \/ ~v 3) /\ (v 3 \/ ~v 2 \/ r) /\ *) 52(* (v 3 \/ v 2 \/ ~r) /\ (~q \/ ~p \/ ~v 2) /\ (p \/ q \/ ~v 2) /\ *) 53(* (v 2 \/ ~p \/ q) /\ (v 2 \/ p \/ ~q) /\ (v 0 \/ ~p \/ ~v 1) /\ *) 54(* (p \/ ~v 0 \/ ~v 1) /\ (v 1 \/ ~p \/ ~v 0) /\ (v 1 \/ p \/ v 0) /\ *) 55(* (r \/ ~q \/ ~v 0) /\ (q \/ ~r \/ ~v 0) /\ (v 0 \/ ~q \/ ~r) /\ *) 56(* (v 0 \/ q \/ r) /\ v 4 *) 57(* ------------------------------------------------------------------------- *) 58 59val PURE_DEF_CNF_VECTOR_CONV : conv 60val DEF_CNF_VECTOR_CONV : conv (* NNF + PURE + CLEANUP *) 61 62val dcnfgv : (unit -> Term.term) ref 63 val ndefs : Term.term ref 64end 65