ML Option
Develop the the following functions, plus any helper functions you need.
 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
productofsums 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 rightassociative 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

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 productofsums form.)

VerifyPI(anyWFF). Here anyWFF is any wellformed formula of the propositional calculus
as specified for ParseFormula.
(It is in productofsums 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 columnheading labels printed that identify
them. For example "~Q v ~R".

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 Prologstyle reasoning
system using Scheme.
 (consult filenamestring). 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")) )

(varfreeproof 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 variablefree 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
(varfreeproof '((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.

(unify literal1 literal2). This should attempt to find a mostgeneral 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.)

(solve query db). This should make use of your unify function as well as the
backtracking search logic of varfreeproof to perform a purelogic 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.
