Harvey Mudd College
Computer Science 60
Assignment 09

Tautology Checker

Due Date: Midnight, morning of Monday April 14

Reading: Chapter 9 in the text.

This assignment is a self-contained Java application that parses logical expressions and indicates which are tautologies. We use the same grammar as in a08. Use your parser, or the one provided in the solution to a08. An example tautology checker using the same grammar, but in applet form, may be found at:

http://www.cs.hmc.edu/~keller/javaExamples/taut/

Requirement: Each expression is one input line. The result is printed following the input. Any number of input expressions can be entered.  For example, if the input is comprised of the following lines, 

(a+b)' = a'*b'
a + a'*b = a + b
a’*a
a’a

then the output will be

(a+b)' = a'*b' is a tautology
a + a'*b = a + b is a tautology
a’*a is not a tautology
a’a is not a well-formed expression

Class LogicTree from a08 should be modified to provide the functionality you need to solve this problem. A lot of the code needed breaks down cleanly along the lines of the class structure in LogicTree.

Class LogicParser from a08 should be copied to class TautologyChecker, then modified to provide the user interface.

Extra Credit:

Once your tautology checker is working, you might consider augmenting it for some extra credit points:

  1. For extra credit worth 20% of the problem, have your analyzer print out whether or not non-tautologies are satisfiable, in the following way:
(a+b)' = a'*b' is a tautology
(a+b)' = a'*b is not a tautology, but is satisfiable
a’*a is not a tautology and is not satisfiable
  1. For extra credit of up to 100% of the problem, depending on capabilities, have your system simplify logic expressions that are not tautologies.  Here I have in mind using rules similar to those for simplifying Binary Decision Diagrams and simple logical equivalences. For example, in the Boole-Shannon expansion, if expression E contains a variable x, then E = x * Ex=1 + x’ * Ex=0. If it happens that Ex=1 = Ex=0, then E can be replaced by the simpler Ex=0. (I don’t suggest that you try to implement hypercube-type simplification, unless you really have lots of time in which to do it properly. ) One useful modification for this version of the program would be to make And and Or trees use lists of arguments, rather than just two arguments. This will allow you to avoid consideration of the order and grouping in which sub-trees are combined with these operators.

Hints and Suggestions:

It is strongly suggested that you use the Boole-Shannon principle recursively to check for tautology. This can be done using either a functional approach or an object-oriented approach. Although the functional approach may require more code and use more memory, it is probably the easiest to get right. The object-oriented approach might be more instructive for variety. However, if you intend to exercise the second extra-credit option, the functional approach is likely to be more manageable for extension.

Using the Boole-Shannon principle means that you will need to add, for example, a method that finds a variable within a LogicTree, if there is one. A good strategy is to declare an abstract method

          Var getVar()

for the abstract class LogicTree, then implement it in derived classes. Have it return null if there is no variable.

If you are using an object-oriented approach, a second useful method is

        void bind(Var var, boolean logicValue)

This would have the effect of binding all instances of var to the indicated value. For this purpose, you would augment the class Var to allow a variable to have a logic value. Your getVar() would actually get an unbound variable in this case. (Use logicValue rather than value to hold a bound value, since the latter is already defined in the Unit base class.) You would also want a method

        void unbind(Var var)

to undo the binding of var.

If instead you are using a functional approach, create a method

        LogicTree subst(Var var, LogicTree value)

that substitutes a constant LogicTree for a var.

Finally, create a method

boolean eval()

of class LogicTree, that would return a boolean value, assuming that every Var has a value. (If some Var does not have a value when eval() is called, then an exception of type UnboundVariableException should be thrown. This is primarily to report internal coding errors.)

NOTE: The helping methods above break down along the lines of the syntax of a LogicTree. However, the method for checking whether an expression is a tautology does not break down in the same way; rather it should be a method defined recursively in the base class only.

Submitting your code: Submit all relevant java files, including the parser.

 
cs60submit *.java
Please make sure that your main program is defined in class TautologyChecker, as this is what our grading program will be expecting.