Week 2-3
Week 6
Week 7
Week 8-9

**Assignments in the lab for the week August 7,
2000 to August 13, 2000:**

Write an ML implementation of *finite sets*, together with the functions
*member*, *subset*, *set equality*, *cartesian
product*, *powerset*, *union*, *intersection*, *set
difference*, *symmetric difference*.

**Assignments in the lab for the week
August 28, 2000 to Sep 3, 2000:**

Choose a representation for variables.

Now, following the template of the first sample program, extend it
to a datatype representing *propositions* built from
variables, and the constant (0-ary) symbols **T** and **F**;
the unary symbol **Not**, and the binary symbols **And**,
**Or**, **Implies** and **Iff**.

Following the template of the second sample program, provide an ML
signature for algebras with the given symbols. Do not use the
lower case names "and", "not", "or", "true" or "false". Also do
not use one-letter names. Use instead the names *truth*,
*falsity*, *negation*, *conjunction*,
*disjunction* , *implication* and *equivalence*
respectively. [Issue: how will you deal with variables?]

Follow the templates of the second and third sample programs to
provide standard syntax and semantics (using the built-in type
*bool* and its values and operations) as well as unparsings
in infix form for propositions. The issue is to be able to
provide a way of representing the unique homomorphic extension
theorem in the given functorial format of sample program 3.

**Assignments in the lab for the week
September 4, 2000 to Sep 10, 2000:**

Write a program *vars* that extract from a proposition, the set
of propositional variables appearing in it.

Write a program *nnf* that converts a proposition to negation normal
form.

Write a program *sop* that converts a given proposition to "sum
of products" normal form.

Write a program *clausify* that converts a given proposition to "product
of sums" normal form.

**Assignments in the lab for the week
September 14, 2000 to Sep 30, 2000:**

Design a SML datatype **sequents**to represent *sequents*
with finite hypotheses, and use it to design a datatype
**deductions** representing *Natural Deductions*.

Write a program *check_ND: deductions -> bool*, that checks if a
value of type *deductions* is indeed a correct Natural Deduction.

Look at the book by Kelly, and represent all the deductions in Theorems 3.1 to 3.13 (pages 47-54), as well as the natural deduction examples given in class of the (S), (K), and (R) tautologies and the Law of the Excluded Middle. Also given several examples of incorrect "deductions".

Write a program *F1: deduction * Prop Set -> deduction* that
given a correct natural deduction *pi* of a sequent "*Gamma |-
psi*", and a finite set of propositions *Gamma'*, returns a
correct natural deduction *pi'* of the sequent "*Gamma U Gamma'
|- psi*". Check that *pi'* is a correct natural deduction.

Write a program *F2: deduction -> deduction* that given a
correct natural deduction *pi* of a sequent "*Gamma |-
psi*", returns a correct natural deduction *pi'* of the
sequent "*Gamma' |- psi*", where *Gamma'* is the smallest
subset of *Gamma* for which the structure and steps of the proof
*pi* will remain unchanged in *pi'*. Check that *pi'*
is a correct natural deduction.
[ Hint: Let *Needed* be set of all the
propositions whose presence is needed in hypotheses of sequents
appearing in *pi* -- e.g., the
conclusions of leaves, the side formulas in the rules like (->I), etc.
Let *Delta = Gamma - Needed*. Subtract *Delta* from each
sequent's hypotheses in deduction *pi*. ]

**Assignments in the lab for the week
October 1, 2000 to October 15, 2000:**

Write a program to implement the **resolution** rule.

Develop a tautology checker that uses resolution repeatedly until the empty clause is added to the collection of clauses. (Hint: take the negation of the formula you want to show is a tautology). You may wish to order the clauses to better direct the resolution process, as also literals within a clause to improve performance.

Using your programs to convert formulae into POS form and to manipulate sets, use resolution to show that instances of the axiom schemes (K) (S) and (R) are provable using resolution.