Harvey Mudd College
Computer Science 60
Assignment 8, Due Thursday, November 4, by midnight

Tautology Checker

or

Knight Identifier

(Link to a tautology checker applet)

The purpose of this assignment is to put the parse trees that result from Assignment 7 to use. Assignment 7, whose solution is available in 

/cs/cs60/assignments/a7/LogicalParser.java.sols ,
parses logical expressions, which may or may not include variables. Such logical expressions fall into 3 broad categories: In this assignment you will write a program that takes a logical expression as input, parses it, and then determines whether or not it is a tautology. For extra credit, you may determine which of the three above categories the expression falls into.

Input/Output behavior

On execution your parser should present the user with a prompt 

Type a logical statement >
at which the user can input arbitrary logical expressions. Logical expresions consist of the symbols described in grammar of Assignment 7. The program should parse that input and then print one of the following lines: 
That expression is a tautology.
That expression is not a tautology.

For example, some correct I/O exchanges include 

Type a logical statement > a+a'
That expression is a tautology.

Type a logical statement > a*a'
That expression is not a tautology.

Type a logical statement > a
That expression is not a tautology.

Type a logical statement > 0 > 1
That expression is a tautology.

Type a logical statement > 1 > 0
That expression is not a tautology.

Suggesions on the coding

Copy your LogicalParser.java code and rename the LogicalParser class to TautChecker. The requirement is that the class which contains the start of the main thread of execution (main) be called TautChecker (so that we can test it easily).

You will want to keep the parsing code as is. You will need the Expr returned from the parsing in order to evaluate the logical expression.

One clean way to approach this problem is to write a single additional function inside the TautChecker class: 

static boolean checkForTaut(Expr e) { ... }
This checkForTaut function will perform Boole-Shannon reduction. That is, it will create two new Exprs by substituting both true and false in for some variable. If both resulting expressions are tautologies, so is the original expression. Otherwise, the original expression is not a tautology.

You will need to add helper functions. One suggestion is to add NO OTHER functions to the TautChecker class, and add the nonstatic functions 

String getAVar()

  - e.getAVar() returns a String that is the variable name of some
    variable appearing in the expression e, it returns null
    if there are no variables in the expression.


Expr substitute(boolean b, String varName)

  - e.substitute(b,varName) returns a new expression in which all
    occurrences of the VarExpr with variable name varName have
    been substituted with with a ConstExpr whose value is the
    boolean b.


evaluate()

  - e.evaluate() returns a boolean which is the value of the
    whole expression e. The expression e must have no
    variables in it; otherwise an error message might be
    printed. (Or you could throw an exception, if you
    want to use exceptions. You don't have to, however.)
to each of the expression classes derived from Expr. In this way, you will be taking advantage of the object-oriented capabilities of Java even more than in Assignment 7. Using the class hierarchy of expressions will save you a lot of work in extending old code (which is one goal of object-oriented programming).

Extra Credit

For extra credit (10 points), have your program categorize the input expression as one of the three types ("tautology", "satisfiable, but not a tautology", or "unsatisfiable") as described above. Thus, a correct run of the program might be 
Type a logical statement > a+a'
That expression is a tautology.

Type a logical statement > a*a'
That expression is unsatisfiable.

Type a logical statement > a
That expression is satisfiable, but not a tautology.

Type a logical statement > 0 > 1
That expression is a tautology.

Type a logical statement > 1 > 0
That expression is unsatisfiable.
Please comment that you're doing this, so that we can test your file appropriately.

Open Problem

The Boole/Shannon reduction described above runs in exponential time with respect to the number of variables in an expression (n). Since a two-way split occurs at each variable, the running time is on the order of 2^n (here "^" means power, not xor).

It is an open question whether or not there exists an algorithm for TautChecker that runs in polynomial time, such as n, n^2, n^3, where n is the number of variables in the expression.

Testing your code

In the /cs/cs60/assignments/a8 directory there are six test files you can use to check that your application is working properly. They are named Test1.in, Test2.in, ..., Test6.in -- and each tests more of the grammar than the previous ones.

To use these files, run 

java TautChecker < /cs/cs60/assignments/a8/Test1.in
(or which ever number you would like to test) and you will see the results of your parser on each of the input lines in that file.

To be sure your output is correct, you can run 

java TautChecker < /cs/cs60/assignments/a8/Test1.in | diff - /cs/cs60/assignments/a8/Test1.out
(for whichever number you're testing). If you see NO output, your parser is producing idential output to the ".out" file. If you do see output, it is a list of the differences between your parser's results and the solutions file.

If you want to check the extra credit problem, the output files are named Test?.ans

Note: If you think you find any errors in the output files, please let me know at dodds@cs.hmc.edu . There shouldn't be, but one never knows... .

Reading

Propositional Logic is covered in Chapter 9 of the text.

Submission

You should submit your TautChecker.java source file in the usual way, i.e., by running 

% cs60submit TautChecker.java
You will be asked to input the assignment number (8).