Assignment 8: Metalogic
CSE 341: Programming Languages
The University of Washington, Seattle, Winter 2012
Purposes: The purposes of this assignment are (1) to gain fluency in either ML or Scheme, and (2) gain experience processing expressions of symbolic logic, which is a fundamental language of computing and mathematics.
Due: Thursday, March 8 at 11:00 PM via Catalyst CollectIt. The target date, however, is March 6.
Individual Work.
This is a partnership assignment. Do this project in teams of 2. Partners are required, for full credit. (Penalty for no partner: -10).
What to Turn In: If you do the ML option, turn in a file If you do the Scheme option, turn in a file If you do the extra-credit Grand-Tour option, also turn in a file plus any additional files needed to run your Grand Tour program. Your file should begin with comment lines that give the name of the file, a program name (that is more descriptive and English-like than the filename), and the authors' (your) names.

ML Option
Develop the the following functions, plus any helper functions you need.
  1. ParseFormula(propFormulaString). This should return a WFF object that is defined by your program to either be an atom, a negation of a WFF, the ANDing together of two WFFs, or the ORing together of two WFFs. Atoms are either propositional constants {T, F}, or variables {P, Q, R, P1, Q1, R1, P2, Q2, R2, P3, Q3, R3 }. You can assume that the string input represents the formula in product-of-sums form. This is closely related to clause form. There may be any number of sums (clauses), and a sum may contain any number of literals (one or more). However, in the ML representation of the formulas, the type constructors orWFF and andWFF should be considered as binary functions, so that, for example, a sum of three literals has to be written with one orWFF nested inside another. In other words, you can consider "v" and "^" to be right-associative binary operators. For example:
    - ParseFormula("P3") ;
    val it = atom("P3") : WFF
    - ParseFormula("P v Q v R") ;
    val it = orWFF(atom("P"), orWFF(atom("Q", atom("R")))) : WFF
    - ParseFormula "(~P v ~Q) ^ (P v R) ^ (~Q v ~R)" ;
    val it = andWFF(orWFF(notWFF(atom("P")), notWFF(atom("Q"))), andWFF(orWFF(atom("P"),atom("R")), 
     orWFF(notWFF(atom("Q")), notWFF(atom("R"))))) : WFF

  3. VerifyTF(tfWFF). We assume tfWFF is a propositional formula string whose atoms are propositional constants (no variables). This function should return either the value tautology or contradiction, depending on whether the formula is true or false, respectively. (As in problem 1, you may assume that the formula is in product-of-sums form.)

  5. VerifyPI(anyWFF). Here anyWFF is any well-formed formula of the propositional calculus as specified for ParseFormula. (It is in product-of-sums form.) This function should return either tautology, contradiction, or underDetermined, depending on whether the formula is always true, always false, or could be either true or false depending upon the values of its variables. This function must use the method of perfect induction (PI) to determine the output. In the course of performing the verification, it should print out the truth table for anyWFF, with a column for each propositional variable that occurs in anyWFF and a column for anyWFF as a whole. Additional columns (for subformulas) are encouraged but optional. If you have them, they should have column-heading labels printed that identify them. For example "~Q v ~R".

  7. VerifyWang(anyWFF). This is optional, for 5 points of extra credit. This should produce the same final result as VerifyPI. However, it should use Wang's algorithm one or more times. Each time one of Wang's rules is applied, your program should announce what rule is being applied and show the new sequent formulas to be proved. If it detects a dead end (sequent with no logical connectives and that is not an axiom), it should terminate the current proof attempt, report that the formula is not a tautology and then try to prove the negation of anyWFF. Depending on these outcomes, it should report one of tautology, contradiction, or underDetermined.

Scheme Option
In this option, your team will implement key parts of a Prolog-style reasoning system using Scheme.
  1. (consult filename-string). This should return a list of Horn clauses, each represented as a list.
    > (consult "grandma.spl")
    (((grandmother x y)(mother x z)(parent z y))
     ((parent x y)(mother x y))
     ((parent x y)(father x y))
     ((mother "Amy" "Bob"))
     ((mother "Carol" "Deb"))
     ((father "Bob" "Erin"))
     ((mother "Deb" "Erin")) )
  2. (var-free-proof query db). This should perform a backtracking search to try to prove the given query using the Horn clauses given in db. You may assume that the particular query and database involve only variable-free terms, so that unifiers either don't exist (i.e., unification fails) or are empty (unification succeeds with no bindings) whenever matching is performed. It should output #t or #f. For example
    (var-free-proof '((father "Bob "Erin")) db)
    should return #t if db is bound to the database above, and assuming variables in the database are ignored or treated as constants. The above database doesn't have any rules (clauses of two or more literals) without variables, but if it did, then your function should be capable of resolving with them, if needed, to answer the query.

  4. (unify literal1 literal2). This should attempt to find a most-general unifier for its two given literals. It should output #f if unification fails, and a list of the form ((var1 term1)(var2 term2) ... (vark termk)) otherwise. (Hint: you will probably find it easier to implement the instructor's version of the unification algorithm than Bezem's.)

  6. (solve query db). This should make use of your unify function as well as the backtracking search logic of var-free-proof to perform a pure-logic evaluation of the query using db. It should report all solutions, unless the set of solutions is infinite, which case it may crash. For each solution, it should list the bindings of those variables that are mentioned in the query.
Grand Tour of CSE 341 (Optional for 10 points of extra credit). Create a Python program that runs your best programs in each of the class's four languages: Python, Prolog, Scheme, ML. In the end, the main Python program should print out the input and output to/from each of the other programs and the amount of time (wall time or CPU time) taken by each of the programs.
Last updated 5 March at 2:27 (VerifyTF also uses the product-of-sums formats explained in the first problem). Previously updated 29 Feb. at 2:57 PM.