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 sequentsto 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.