Predicate calculus

The deduction rules are then adapted to the new language:

• Introduction rule

let intro h = function
 | (hs,(I(p,q))::ps) -> ((h,p)::hs,q::ps)
 | s                 -> s;;

let s2 = proof p |> intro "h1" |> intro "h2";; // = ???

• Application rule

let apply h (hs,p::ps) = 
 let v = List.filter (fun (k,r)->k=h) hs
 match v,p with
 | (_,I (P h,P q))::_,P r -> match unify q r [] with
                             | (true,ctx)-> (hs,(P (eval h ctx))::ps) 
                             | _           ->  (hs,p::ps)
 | (_,q)::_ ,_            -> if p=q then  (hs,ps) else  (hs,p::ps)
 | _,_                    ->  (hs,p::ps);;

s2 |> apply "h2" |> apply "h1" |> qed;; // = ???

Nb. In the preceding code, unify has to implement an unification algorithm (e.g. between ["Man","Socrate"] and ["Man","?x"]) and is left as en exercise.
As a complement, eval use a context (e.g. [("?x","Socrate")]) to evaluate an expression (e.g. ["Mortal","?x"]).
Nb2. The source code of these functions can be found here and can be loaded in interpreted mode with

#load "Unify.fs";;
open Unify.Unify;;

11 - 12