Functional Programming & Proofs

Predicate calculus

The deduction rules are now: "intro x" and "apply" but with rewriting.

type P = P of string list | I of (P * P);; // Predicates
let (=>) x y = I (x,y);;
let p = P ["Man";"Socrate"] 
        => ((P ["Man";"?x"] => P ["Mortal";"?x"]) 
        => P ["Mortal";"Socrate"]);;

Sequents have then to be changed to:

type Sq   = ((string*P) list) * (P list);;

let proof (p:P):Sq = ([],[p]);;
let qed = function
  | (_,[]) -> "proof conplete."
  | _      -> "not finished.";;

10 - 12