CPSC 415 SML Programming Assignment 2
		
	      Due Date: At least some part due next week


Part I:

  For this assignment, you are asked to expand on the code we went over
in class to build an *automated* theorem prover for the propositional
(quantifier-free) fragment of the intuitionistic sequent calculus.  You
are to define a function

	fun autoprove S = ...  (type should be sequent -> unit)

that takes a sequent S and attempts to prove it.  You should print out
the intermediate steps so we'll have a clue as to what your prover is
trying to do.  If no proofs are found, you are to report failure.

  Your program must be able to find proofs to AT LEAST ALL THE
NEGATION-FREE INTUITIONISTIC PROPOSITIONAL TAUTOLOGIES (a tautology is
a formula provable from no assumptions, i.e., []|-A).  The trick is to
exploit the "nice" property of the LJ calculus given by the Cut
Elimination result:

  *If []|-A is provable then the last rule is a right logical rule.*

  Even when the left hand side of the sequent is not empty, you should
still try to apply right-rules first.  A proof where right-rules are
applied whenever possible, except when Id is applicable, is called
a "Uniform Proof."

  Additional hints: there will be times when your theorem prover
chooses to apply a wrong rule (e.g., impL instead of orL).  You might
want to define a funciton "attempt" that will return the original goal
should whatever you've tried to attempt fail.  Avoid the Contraction
rule as that will lead to divergence.  You will need to figure out how
and when to use the Exchange rule - you may want to incorporate
exchange into your rules so that they search the left-hand side of a
sequent for anything appropriate.  Basically, the exchange rule allows
you to attempt a left-rule on any formula on the left hand side of sequent.


Part II:

  If you feel confident enough, you should do part II without doing
part I, though I strongly recommed against it.  Though proving a
theorem automatically is nice, it would be nicer if we could extract
the "computational content" of the proofs constructed.  You are to
modify your program from part I so that it will *return* the proof
found by your program. Proofs can be represented as compositions of
the left and right rules.  The proof returned should be usable as a
new rule, capable of proving your theorem in one step.

  The type of your new autoprove function should be

        (sequent -> (sequent -> sequent list))

  Hints:  You *might* find the following useful:

(* ----------------------------------------------------------------------*)
(* function composition is built into ML as (F o G) *)
(* A proof in the sequent calculus is now a composition of the functions andR, impL, etc...
   In other words, a proof is a also a function, or PROGRAM!!!!! *)

(* the "parade" higher order function applies a list of functions to 
   a list of arguments respectively *)
fun parade nil l = nil
  | parade l nil = nil
  | parade (ff::ft) (h::ht) = (ff h)::(parade ft ht);

(* "expand" expands out all the subgoals returned by parade *)
fun expand fs ls = flat (parade fs ls);

(* the higher order function "try" tries a list of rules until one works *)
fun try nil Goal = [Goal]
  | try (h::t) Goal = let val P = (h Goal) in
	if (P=nil) then nil else
	  let val (a::G) = P in
	    if (Goal = a) then (try t Goal)
	      else P 
    	  end
	end;

val Rules = [Id, andR, (orR 1), (orR 2), impR, negR, impL, (andL 1), (andL 2), orL, negL];
(* ----------------------------------------------------------------------*)


   Using this representation, the proof for the sequent [r0-:s0,r0]|-s0
is 

      		(expand [Id, Id]) o (impL)  

 That is, "modus ponens" can be proved by applying the impL rule
followed by the Id rule to each of the subgoals.  The composition
above will now allow us to apply modus ponens in *one* step.