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
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
-
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.)
-
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".
-
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.
- (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")) )
-
(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.
-
(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.)
-
(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.
|
