(* Espressions *)
type exp =
Num of int
(* deBruijn: variables are numbers *)
| Var of int
| Plus of exp * exp
(* Formulae *)
type form =
Forall of form
| Exists of form
| Imp of form * form
| Neg of form
| True
| False
| Eq of exp * exp
(* Modify the index of the variables (Var n) in an espression and
if n < th then (Var (n+i))
otherwise (Var (n+o)) *)
let rec shiftExp th i o e = match f with
Num n -> Num n
| Var n -> if (n < th) then Var (n+i) else Var (n+o)
| Plus (e1, e2) -> Plus ((shiftExp th i o e1), (shiftExp th i o e2))
(* Modify the index of the variables (Var n) in a formula f
If n < then (Var (n+i))
Otherwise (Var (n+o)) *)
let rec shiftForm th i o f = match f with
Forall f1 -> Forall f1
| Exists f1 -> Exists f1
| Imp (f1, f2) -> Imp ((shiftForm th i o f1), (shiftForm th i o f2))
| Neg f1 -> Neg (shiftForm th i o f1)
| True -> True
| False -> False
| Eq (e1, e2) -> Eq ((shiftExp th i o e1), (shiftExp th i o e2))
(* negation *)
let rec lift_neg f = match f with
Forall f1 -> Exists (lift_neg f1)
| Exists f1 -> Forall (lift_neg f1)
| Neg f1 -> f1
| True -> False
| False -> True
| _ -> Neg f
(* implication *)
let lift_if f1 f2 =
let rec lift_if1 n m f1 f2 = match f2 with
Forall b -> Forall (lift_if1 n (S m) f1 b)
| Exists b -> Exists (lift_if1 n (S m) f1 b)
| _ -> Imp ((shiftForm n m m f1), (shiftForm m O n f2))
in
let rec lift_if2 n f1 f2 = match f1 with
Forall b -> Exists (lift_if2 (S n) b f2)
| Exists b -> Forall (lift_if2 (S n) b f2)
| _ -> lift_if1 n O f1 f2
in
lift_if2 O f1 f2
(* Main function *)
let rec lift_quant f = match f with
Forall f1 -> Forall (lift_quant f1)
| Exists f1 -> Exists (lift_quant f1)
| Imp (f1, f2) -> lift_if (lift_quant f1) (lift_quant f2)
| Neg f1 -> lift_neg (lift_quant f1)
| _ -> f
type form1 = FOR of form1 | EX of form1 | AND of form1 * form1 | OR of form1 * form1 | NEG of form1 | TRUE | FALSE | EQ of exp * exp | CONG of int * exp * exp (* From form to form1 *) let rec form_to_form1 f = match f with Forall f1 -> FOR (form_to_form1 f1) | Exists f1 -> EX (form_to_form1 f1) | Neg f1 -> NEG (form_to_form1 f1) | Imp (f1, f2) -> OR (NEG (form_to_form1 f1), form_to_form1 f2) | True -> TRUE | False -> FALSE | Eq (e1,e2) -> EQ (e1,e2)
(* RIght Distributivity *)
let rec push_and_rules1 f1 f2 = match f1 with
OR (f3, f4) -> OR (push_and_rules1 f3 f2, push_and_rules1 f4 f2)
| _ -> AND (f1, f2)
(* Left Distributivity *)
let rec push_and_rules f1 f2 = match f2 with
OR (f3, f4) -> OR (push_and_rules f1 f3, push_and_rules f1 f4)
| _ -> push_and_rules1 f1 f2
(* Distributivity; *)
let rec push_and f = match f with
AND (f1, f2) -> push_and_rules (push_and f1) (push_and f2)
| OR (f1, f2) -> OR (push_and f1, push_and f2)
| _ -> f
(* Negation of modulo into disjunction *)
let rec expand_NEG_CONG i a b n = match n with
0 -> FALSE
| 1 -> CONG (i, a, Plus (b, Num n))
| _ -> OR (CONG (i, a, Plus (b, Num n)),
expand_NEG_CONG i a b (n-1))
(* Push down negation *)
let rec push_neg b f = match b,f with
true, AND (f1, f2) -> AND ((push_neg true f1), (push_neg true f2))
| true, OR (f1, f2) -> OR ((push_neg true f1), (push_neg true f2))
| true, NEG f1 -> push_neg false f1
| true, _ -> f
| false, AND (f1, f2) -> OR ((push_neg false f1), (push_neg false f2))
| false, OR (f1, f2) -> AND ((push_neg false f1), (push_neg false f2))
| false, NEG f1 -> push_neg true f1
| false, TRUE -> FALSE
| false, FALSE -> TRUE
| false, CONG (0, e1, e2) -> NEG (EQ (e1, e2))
| false, CONG (1, e1, e2) -> FALSE
| false, CONG (i, e1, e2) -> expand_NEG_CONG i e1 e2 (i-1)
| false, _ -> NEG f
(* dnf *)
let dnf f = push_and (push_neg true f)
(* Expand forall *)
let rec expand_forall b f = match (b,f) with
true, FOR f1 -> NEG (EX (expand_forall false f1))
| true, EX f1 -> EX (expand_forall true f1)
| true, _ -> dnf f
| false, FOR f1 -> EX (expand_forall false f1)
| false, EX f1 -> NEG (EX (expand_forall true f1))
| false, _ -> dnf (NEG f)
(* prenex DNF for form1 *)
let normal_form f = expand_forall true (form_to_form1 (lift_quant f))
(x ∧¬z) ∨ (¬y ∧ ¬z)
*H6
Put the formula ¬((∃x. (P x)) ⇒(∀x. (Q x))) in DNF.
∃x.∃y.((P x) ∧¬(Q x))
*H7
Put the formula (∀x.∃y. (P x y)) ⇒(∃x. (P x x)) in DNF.
∃x.∀y.∃z. ¬(P x y) ∨(P z z)
H8
Write a function decide_ground
that decides if a formula of type form1 without variable is true.
(* Decide if a modulo is true *) let cong_dec i a b = match i with 0 -> a=b | _ -> (a-b) mod i =0 (* Evaluate an expression in an environment *) let rec exp_to_int l e = match e with Num n -> n | Var n -> List.nth l n | Plus (e1, e2) -> (exp_to_int l e1)+(exp_to_int l e2) (* Decide a ground expression *) let rec decide_ground f = match f with FOR b -> false | EX b -> false | AND (f1, f2) -> if decide_ground f1 then decide_ground f2 else false | OR (f1, f2) -> if decide_ground f1 then true else decide_ground f2 | NEG f1 -> not (decide_ground f1) | TRUE -> true | FALSE -> false | EQ (e1, e2) -> (exp_to_int [] e1) = (exp_to_int [] e2) | CONG (i, e1, e2) -> cong_dec i (exp_to_int [] e1) (exp_to_int [] e2)
(* Factorise Var 0 in an expression *)
let rec factor_var e = match e with
Num i -> 0, e
| Var 0 -> 1, Num 0
| Var n -> 0, Var (n-1)
| Plus (e1, e2) ->
let m1,e3 = factor_var e1 in
let m2,e4 = factor_var e2 in
(m1+m2), Plus (e3, e4)
(* Factorise Var 0 in a formula *)
let factor_exp f = match f with
EQ (e1, e2) ->
let m1,e3 = factor_var e1 in
let m2,e4 = factor_var e2 in
if (m1
let m1,e3 = factor_var e1 in
let m2,e4 = factor_var e2 in
if (m1
let m1,e3 = factor_var e1 in
let m2,e4 = factor_var e2 in
if (m1 0,f
(* Modulo with modulo *)
let rec reduce_CONG_CONG1 i m1 m2 a1 a2 b1 b2 =
if (m1=m2) then (m1,a1,b1, CONG (i, Plus (a2, b1), Plus (b2, a1)))
else if m1 < m2 then
reduce_CONG_CONG1 i m1 (m2-m1) a1 (Plus (a2, b1)) b1 (Plus (b2, a1))
else
reduce_CONG_CONG1 i m2 (m1-m2) a2 (Plus (a1, b2)) b2 (Plus (b1, a2))
(* Scalar product *)
let rec scal n e = match n with
0 -> Num 0
| 1 -> e
| _ -> Plus (e, (scal (n-1) e))
(* Modulos with modulo *)
let rec reduce_CONG_CONG i1 m1 a1 b1 l = match l with
(m2,CONG (i2, a2, b2))::l1 ->
let (i4, a4,b4,f4) =
reduce_CONG_CONG1 (lcm i1 i2) (((lcm i1 i2)/i1)*m1)
(((lcm i1 i2)/ i2) * m2)
(scal ((lcm i1 i2)/i1) a1)
(scal ((lcm i1 i2)/i2) a2)
(scal ((lcm i1 i2)/i1) b1)
(scal ((lcm i1 i2)/i2) b2) in
let (i5, m5, a5, b5, l5) =
reduce_CONG_CONG (lcm i1 i2) i4 a4 b4 l1 in
(i5, m5, a5, b5, f4::l5)
| _ -> (i1,m1,a1,b1,[])
(* Equations with equation *)
let rec reduce_EQ_EQ m1 a1 b1 l = match l with
(m2,EQ (a2, b2))::l1 ->
(EQ (Plus (scal ((lcm m1 m2)/m1) b1, scal ((lcm m1 m2)/m2) a2),
Plus (scal ((lcm m1 m2)/m1) a1, scal ((lcm m1 m2)/m2) b2)))
::reduce_EQ_EQ m1 a1 b1 l1
| _ -> []
(* Negations with equation *)
let rec reduce_EQ_NEQ m1 a1 b1 l = match l with
(m2,NEG (EQ (a2, b2)))::l1 ->
(NEG (EQ (Plus (scal ((lcm m1 m2)/m1) b1, scal ((lcm m1 m2)/m2) a2),
Plus (scal ((lcm m1 m2)/m1) a1, scal ((lcm m1 m2)/m2) b2))))
::reduce_EQ_NEQ m1 a1 b1 l1
| _ -> []
(* Moduli with equation *)
let rec reduce_EQ_CONG m1 a1 b1 l = match l with
(m2,CONG (n, a2, b2))::l1 ->
(CONG (((lcm m1 m2)/m2)* n,
Plus (scal ((lcm m1 m2)/m1) b1, scal ((lcm m1 m2)/m2) a2),
Plus (scal ((lcm m1 m2)/m1) a1, scal ((lcm m1 m2)/m2) b2)))
::reduce_EQ_CONG m1 a1 b1 l1
| _ -> []
(* Reductions *)
let process_list l = match l with
(l1,[],(m1,CONG (i1,a1,b1))::l3,l4) ->
let (i2,m2,a2,b2,l5) = reduce_CONG_CONG i1 m1 a1 b1 l3 in
(CONG (gcd i2 m2, a2, b2))::(List.append l1 l5)
| (l1,(m1,(EQ (a1, b1)))::l2,l3,l4) ->
(CONG (m1, a1, b1))::
(List.append l1
(List.append (reduce_EQ_EQ m1 a1 b1 l2)
(List.append (reduce_EQ_CONG m1 a1 b1 l3)
(reduce_EQ_NEQ m1 a1 b1 l4))))
| (l1,_,_,_) -> l1
(* Return 4 lists:
- the formulae that do not contain Var 0
- all the equations
- all the modulos
- all the negations of equations
*)
let rec sort_and f = match f with
| EQ (e1, e2) ->
let n, f1 = factorExp f in
if (n=0) then [f1],[],[],[]
else [],[n,f1],[],[]
| NEG (EQ (e1, e2)) ->
let n, f1 = factorExp f in
if (n=0) then [f1],[],[],[]
else [],[],[],[n,f1]
| CONG (n, e1, e2) ->
if n=0 then
begin
let n1, f1 = factorExp (EQ (e1, e2)) in
if n1=0 then [f1],[],[],[] else [],[n,f1],[],[]
end
else
begin
let n1, f1 = factorExp f in
if n1=0 then [f1],[],[],[] else [],[],[n,f1],[]
end
| AND (f1, f2) ->
let (l1,l2,l3,l4) = sort_and f1 in
let (l'1,l'2,l'3,l'4) = sort_and f2 in
(List.append l1 l'1, List.append l2 l'2, List.append l3 l'3, List.append l4 l'4)
| f -> [f],[],[],[]
(* List of formulae into a single conjunction *)
let rec build_conj = function
[] -> TRUE
| [e] -> e
| e :: l1 -> AND (e, (build_conj l1))
(* Eliminate var 0 *)
let rec elim_quant f = match f with
OR (f1, f2) -> OR ((elim_quant f1), (elim_quant f2))
| _ -> build_conj (process_list (sort_and f))
(* Eliminate all the variables *) let rec elim_quants f = match f with EX f1 -> elim_quant (elim_quants f1) | NEG (EX f1) -> dnf (NEG (elim_quant (elim_quants f1))) | _ -> f