-
Notifications
You must be signed in to change notification settings - Fork 1
/
skolems.ml
27 lines (22 loc) · 928 Bytes
/
skolems.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
(* ========================================================================= *)
(* Illustration of Skolemizing a set of formulas *)
(* *)
(* Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.) *)
(* ========================================================================= *)
let rec rename_term tm =
match tm with
Fn(f,args) -> Fn("old_"^f,map rename_term args)
| _ -> tm;;
let rename_form = onformula rename_term;;
let rec skolems fms corr =
match fms with
[] -> [],corr
| (p::ofms) ->
let p',corr' = skolem (rename_form p) corr in
let ps',corr'' = skolems ofms corr' in
p'::ps',corr'';;
let skolemizes fms = fst(skolems fms []);;
START_INTERACTIVE;;
skolemizes [<<exists x y. x + y = 2>>;
<<forall x. exists y. x + 1 = y>>];;
END_INTERACTIVE;;