<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
open List;;

type pred = int;;

type var = int;;

type term = var;;

type form = 
  | Eq of term * term
  | NEq of term * term
  | Atom of (pred*(term list))
  | NAtom of (pred*(term list))
  | FConj of form * form
  | FDisj of form * form
  | FAll of form
  | FEx of form;;

let rec preSuc t = match t with
  | [] -> []
  | (a::list) -> (match a with 0 -> preSuc list | sucn -> (sucn-1::preSuc list))
;;

let rec fv t = match t with
  | Eq (p,q) -> [p;q]
  | NEq (p,q) -> [p;q]
  | Atom (p,vs) -> vs
  | NAtom (p,vs) -> vs
  | FConj (f,g) -> (fv f)@(fv g)
  | FDisj (f,g) -> (fv f)@(fv g)
  | FAll f -> preSuc (fv f)
  | FEx f -> preSuc (fv f)
;;

let suc x = x+1;;

let rec subst r f = match f with 
  | Eq (p,q) -> Eq(r p, r q)
  | NEq (p,q) -> NEq(r p, r q)
  | Atom (p,vs) -> Atom (p,map r vs)
  | NAtom (p,vs) -> NAtom (p,map r vs)
  | FConj (f,g) -> FConj (subst r f, subst r g)
  | FDisj (f,g) -> FDisj (subst r f, subst r g)
  | FAll f -> FAll (subst (fun y -> match y with 0 -> 0 | sucn -> suc (r (sucn - 1))) f)
  | FEx f -> FEx (subst (fun y -> match y with 0 -> 0 | sucn -> suc (r (sucn - 1))) f);;

let finst body w = subst (fun v -> match v with 0 -> w | sucn -> (sucn-1)) body;;

let sfv s = flatten (map fv s);;

let rec maxvar t = match t with
    [] -> 0
  | (a::list) -> max a (maxvar list);;

let newvar vs = suc (maxvar vs);;

let update e s t = let u = min (e s) (e t) in fun x -> if e x = e s || e x = e t then u else e x;;

(* get the first equivalence class not already used to instantiate a forall quantifier *)
let rec next e n = if e n = n then n else next e (suc n);;

type seq = form list;;

type nseq = (int * form) list;;

(* the second component is a function that reduces a term to a normal form, given the equalities observed so far on the branch *)
type eseq = nseq * (term -> term);;

(* in following, t is a sequent of numbered formulae *)
(* %%cut subs *)
let subs ((t,e):eseq) = match t with 
  | [] -> ([([],e)]:eseq list) 
  | (x::xs) -> 
      let (m,f) = x in 
	(match f with
	   | Eq (s,t) -> [(xs,update e s t)]
	   | NEq (s,t) -> 
	       let (s,t) = (e s, e t) in 
		 if s = t then [] else [(xs@[0,NEq(s,t)],e)]
	   | Atom(p,vs) -> 
	       let vs' = map e vs in
		 if mem (NAtom(p,vs')) (map snd xs) then []
		 else [(xs@[(0,Atom(p,vs'))],e)]
	   | NAtom(p,vs) -> 
	       let vs' = map e vs in 
		 if mem (Atom(p,vs')) (map snd xs) then [] 
		 else [(xs@[(0,NAtom(p,vs'))],e)]
	   | FConj (f,g) -> let t' = xs@[(0,f);(0,g)] in [(t',e)]
	   | FDisj (f,g) -> [(xs@[(0,f)],e);(xs@[(0,g)],e)]
	   | FAll f -> let m' = next e m in let t' = xs@[(0,finst f m');(suc m',FAll f)] in [(t',e)]
	   | FEx f -> let t' = xs@[(0,finst f (newvar (sfv (map snd (x::xs)))))] in [(t',e)])
;;
(* %%tuc *)

let step (l:eseq list) = flatten (map subs l);;

(* %%cut prove' *)
let rec prove' (l:eseq list) = match l with [] -> true | _ -> prove' (step l)
;;
(* %%tuc *)

(* %%cut prove *)
let prove (s:seq) = prove' [(map (fun x -> (0,x)) s,fun x -> x)];;
(* %%tuc *)

(* sample formula *)
(* want to prove |- (? x y. ! z. z = x | z = y) --> (! x y z. x = y | y = z | z = x) *)

(* i.e. (? x y. ! z. z = x | z = y), ~ (! x y z. x = y | y = z | z = x) |- *)
(* i.e. (? x y. ! z. z = x | z = y), ? x y z. x ~= y & y~=z & z ~= x |- *)
(* i.e. (? x y. ! z. z = x | z = y) & ? x y z. x ~= y & y~=z & z ~= x |- *)

let c1 = FEx (FEx (FAll (FDisj (Eq(0,2),Eq(0,1)))));;
let c2 = FEx (FEx (FEx (FConj (FConj(NEq(2,1), NEq(1,0)),NEq(0,2)))));;
let c3 = FConj (c1,c2);;

let s1 = [c3];;
let ns1 = (map (fun x -> (0,x)) s1);;
let es1:eseq = (ns1,fun x -> x);;

prove s1;;

(* |- (? x. P x) & (? x. Q x) & (! x y. x = y) --> (? x. P x & Q x) *)
(* (? x. P x) & (? x. Q x) & (! x y. x = y), ~ (? x. P x & Q x) |- *)
(* (? x. P x) & (? x. Q x) & (! x y. x = y), (! x. ~ P x | ~ Q x) |- *)

let c1 = FEx (Atom (1,[0]));;
let c2 = FEx (Atom (2,[0]));;
let c3 = FAll (FAll (Eq(0,1)));;
let c4 = FAll(FDisj((NAtom(1,[0]),NAtom(2,[0]))));;

let s1=[c1;c2;c3;c4];;
let ns1 = (map (fun x -> (0,x)) s1);;
let es1:eseq = (ns1,fun x -> x);;

prove s1;;


(* something that shouldn't be provable *)
(* |- (! x y. x = y) --> (? x. P x & Q x) *)
(* (! x y. x = y), (! x. ~ P x | ~ Q x) |- *)

let s1=[c3;c4];;
let ns1 = (map (fun x -> (0,x)) s1);;
let es1:eseq = (ns1,fun x -> x);;

prove s1;;