Commit 0ea5771b authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

The file

parents
type term = Var of string
| Funct of string * term list
type prop = Atomic of string * term list
| Neg of prop
| Imp of prop * prop
| Conj of prop * prop
| Disj of prop * prop
| Exist of string * prop
| Univ of string * prop
let rec string_of_prop : prop -> string =
let rec string_of_var =
function
| Var s -> s
| Funct(f,l) -> f ^ "(" ^ (String.concat "," (List.map string_of_var l)) ^ ")"
in
function
| Atomic (str,l) -> str ^ "(" ^ (String.concat "," (List.map string_of_var l)) ^ ")"
| Neg a -> "~(" ^ (string_of_prop a) ^ ")"
| Imp (a,b) -> "(" ^ (string_of_prop a) ^ "=>" ^ (string_of_prop b) ^ ")"
| Conj (a,b) -> "(" ^ (string_of_prop a) ^ "/\\" ^ (string_of_prop b) ^ ")"
| Disj (a,b) -> "(" ^ (string_of_prop a) ^ "\\/" ^ (string_of_prop b) ^ ")"
| Exist (str,b) -> "(Ex " ^ str ^ "." ^ (string_of_prop b) ^ ")"
| Univ (str,b) -> "(Pr tt " ^ str ^ "." ^ (string_of_prop b) ^ ")"
let examples =
[Exist ("x",(Imp (Atomic ("P",[Var "x"]),Atomic ("P",[Var "x"]))));
Exist ("x", Exist ("y",
(Imp (Atomic ("P",[Var "x"]), Atomic ("P",[Funct ("f",[Var "y"])])))));
Exist("x",Imp
(Conj
(Imp (Atomic("P",[Var "x"]),Atomic("P",[Funct("f",[Var "x"])])),
Atomic("P",[Funct ("a",[])])),
Atomic("P",[Funct ("f",[Funct ("a",[])])])));
Exist ("x",
(Imp (Atomic ("P",[Funct ("f",[Var "x"])]),
Atomic ("P",[Funct ("g",[Var "x"])]))))
]
let rec subst : (term * term) list -> term -> term =
fun s t ->
match t with
| (Var str) -> (try List.assoc (Var str) s with Not_found -> t)
| (Funct (str,l)) -> Funct (str,List.map (subst s) l)
let rec subst_prop : (term * term) list -> prop -> prop =
fun s ->
function
| Atomic (str,l) -> Atomic (str,List.map (subst s) l)
| Neg a -> Neg (subst_prop s a)
| Imp (a,b) -> Imp (subst_prop s a,subst_prop s b)
| Conj (a,b) -> Conj (subst_prop s a,subst_prop s b)
| Disj (a,b) -> Disj (subst_prop s a,subst_prop s b)
| Exist (str,b) -> Exist (str,subst_prop s b)
| Univ (str,b) -> Univ (str,subst_prop s b)
exception FreshnessCondition
let rec permute : prop list -> prop list =
fun l ->
let rec permute_rec ll = function
| [] -> ll
| (Atomic (str,arg))::l' -> permute_rec ((Atomic(str,arg))::ll) l'
| p::l' -> p::(ll @ l')
in permute_rec [] l
let rec der : prop list -> prop list -> (prop list * prop list) list =
fun gamma delta ->
(* TODO *)
match (permute gamma, permute delta) with
| (gamma', delta') -> [(gamma',delta')]
let subst_eq : (term * term) list -> (term * term) -> term * term=
fun s (a,b) -> (subst s a, subst s b)
exception Unif
let rec occur : string -> term -> bool =
(* TODO *)
fun x t -> true
let rec unif : (term * term) list -> (term * term) list=
(* TODO *)
function
| [] -> []
| (Var x , Var y) :: l ->
l
| (Var x , t) :: l ->
l
| (t , Var x) :: l ->
l
| (Funct (str1,l1), Funct (str2,l2)):: l ->
l
let rec unif_atomic_prop : prop -> prop -> (term * term) list =
fun a1 a2 ->
match (a1,a2) with
| (Atomic (str1,l1), Atomic (str2,l2)) ->
if str1 = str2
then (unif (List.combine l1 l2))
else raise Unif
| _ -> assert false
let subst_seq : (term * term) list -> (prop list * prop list) -> (prop list * prop list) =
fun s (gamma,delta) ->
(List.map (subst_prop s) gamma, List.map (subst_prop s) delta)
let rec axiom : (prop list * prop list) list -> bool =
function
| [] -> true
| ((gamma,delta)::l) -> axiom' gamma delta l
and axiom' : prop list -> prop list -> (prop list * prop list) list -> bool =
fun gamma delta l ->
match gamma with
| [] -> false
| (a::gamma') -> (axiom'' a delta l) || (axiom' gamma' delta l)
and axiom'' : prop -> prop list -> (prop list * prop list) list -> bool =
fun a delta l ->
match delta with
| [] -> false
| (b::delta') ->
(try let s = unif_atomic_prop a b in axiom (List.map (subst_seq s) l)
with Unif -> false)
|| (axiom'' a delta' l)
let derivable : prop -> bool =
fun p -> axiom (der [] [p])
let _ =
List.iter
(fun p -> Format.printf "%s %B@." (string_of_prop p) (derivable p))
examples
let rec fetch_quantif : prop -> prop =
function
| Neg (Exist (str,b)) -> Univ (str, fetch_quantif (Neg b))
| Neg (Univ (str,b)) -> Exist (str, fetch_quantif (Neg b))
| Imp (Univ (str,a),b) -> Exist (str, fetch_quantif (Imp (a,b)))
| Imp (Exist (str,a),b) -> Univ (str, fetch_quantif (Imp (a,b)))
| Imp (a,Univ (str,b)) -> Univ (str, fetch_quantif (Imp (a,b)))
| Imp (a,Exist (str,b)) -> Exist (str, fetch_quantif (Imp (a,b)))
| Conj (Univ (str,a),b) -> Univ (str, fetch_quantif (Conj (a,b)))
| Conj (Exist (str,a),b)-> Exist (str, fetch_quantif (Conj (a,b)))
| Conj (a,Univ (str,b)) -> Univ (str, fetch_quantif (Conj (a,b)))
| Conj (a,Exist (str,b))-> Exist (str, fetch_quantif (Conj (a,b)))
| Disj (Univ (str,a),b) -> Univ (str, fetch_quantif (Disj (a,b)))
| Disj (Exist (str,a),b)-> Exist (str, fetch_quantif (Disj (a,b)))
| Disj (a,Univ (str,b)) -> Univ (str, fetch_quantif (Disj (a,b)))
| Disj (a,Exist (str,b))-> Exist (str, fetch_quantif (Disj (a,b)))
| t -> t
let rec prenex : prop -> prop =
(* TODO *)
function
| Atomic (str,l) as t -> t
| Neg a -> a
| Imp (a,b) -> a
| Conj (a,b) -> a
| Disj (a,b) -> a
| Exist (str,b) -> b
| Univ (str,b) -> b
let distrib : prop list list -> prop list list -> prop list list =
fun a b ->
let f l1 = List.map (List.append l1) a in
List.fold_left (fun acc l -> acc @ f l) [] b
let rec clausal : prop -> prop list list =
(* TODO *)
function
| Atomic (str,l) as p -> [[p]]
| Neg (Atomic (str,l)) as p -> [[p]]
| Neg (Neg a) -> [[a]]
| Neg (Imp(a,b)) -> [[a]]
| Neg (Conj(a,b)) -> [[a]]
| Neg (Disj(a,b)) -> [[a]]
| Imp (a,b) -> [[a]]
| Conj (a,b) -> [[a]]
| Disj (a,b) -> [[a]]
| Exist (str,b) -> [[b]]
| Univ (str,b) -> [[b]]
| _ -> assert false (* This function is only applied to prenex proposition *)
let rec remove : 'a -> 'a list -> 'a list =
fun x ->
function
| [] -> []
| a :: l when (a=x) -> remove x l
| a :: l -> a :: (remove x l)
let rec free_var_term : term -> string list =
(* TODO *)
function
| Var s -> [""]
| Funct (s,l) -> [""]
let rec free_var : prop -> string list =
(* TODO *)
function
| Atomic (str,l) -> [""]
| Neg a -> [""]
| Imp (a,b) -> [""]
| Conj (a,b) -> [""]
| Disj (a,b) -> [""]
| Exist (str,b) -> [""]
| Univ (str,b) -> [""]
let rec replace : string -> term -> prop -> prop =
let rec replace_term : string -> term -> term -> term =
fun x t ->
function
| Var s -> if s=x then t else Var s
| Funct (s,l) -> Funct(s,List.map (replace_term x t) l)
in
fun x t ->
function
| Atomic (str,l) -> Atomic (str, List.map (replace_term x t) l)
| Neg a -> Neg (replace x t a)
| Imp (a,b) -> Imp (replace x t a,replace x t b)
| Conj (a,b) -> Conj (replace x t a,replace x t b)
| Disj (a,b) -> Disj (replace x t a,replace x t b)
| Exist (str,b) -> Exist (str,replace x t b)
| Univ (str,b) -> Univ (str,replace x t b)
let skolemise : prop -> prop =
let rec skolemise_rec : int -> prop -> prop =
fun i ->
function
| Univ (str,b) -> skolemise_rec i b
| Exist (str,b) ->
begin
let
(* TODO *)
l = []
in
let t=Funct("sk"^(string_of_int i),l) in
skolemise_rec (i+1) (replace str t b)
end
| t -> t
in skolemise_rec 0
let clausal_skolemise : prop -> prop list list =
fun p ->
List.map (fun l -> List.map skolemise l) (clausal (prenex p))
let string_of_clause_set l =
List.fold_left (fun st x -> let y= "["^x^"]" in
if (st="") then y else st ^ "/\\" ^ y) ""
(List.map
(List.fold_left (fun st x -> let y =string_of_prop x in
if (st="") then y else st ^ "\\/" ^ y) "")
l
)
let _ =
List.iter
(fun p -> Format.printf "%s become@. %s@."
(string_of_prop p)
(string_of_clause_set (clausal_skolemise p))
)
examples
let rec factorisation : prop list -> prop list =
function
| [] -> []
| a :: l -> if List.mem a l then (factorisation l) else a::(factorisation l)
exception NoUnif
exception Success of (term * term) list * prop * prop
let resolution : prop list -> prop list -> prop list =
(* TODO *)
fun l1 l2 -> l1
let def : prop =
Conj (Atomic ("",[Var ""]),Atomic ("",[Var ""]))
let rec resolution_proof : prop list list -> prop list list -> bool =
fun l_old l_new ->
Format.printf "%s@." (string_of_clause_set l_new);
if l_new=[] then false else
if List.mem [] l_new then true
else
(* TODO *)
let l_res = []
in resolution_proof (l_old @ l_new) l_res
let derivable_resol : prop -> bool =
fun p ->
resolution_proof [] (clausal_skolemise (Neg p))
let _ =
List.iter
(fun p -> Format.printf "%s %B@." (string_of_prop p) (derivable_resol p))
examples
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment