If you have taken the functional language class, then you must do the project in Racket or OCaml.

Due:

Design a Haskell data type for representing formulas in propositional logic. The program is to read in a formula of propositional logic and determine if the formula is a tautology and write the formula out in conjunctive normal form.

The principle steps are:

• Design a Haskell data type for representing formulas in propositional logic.
• Read strings from the standard input stream which represent the formula in a postfix notation.
• Write a recursive function to convert the formula to negation normal form.
• Write a recursive function to convert a formula in negation formal form to conjunctive normal form.
• Write a recursive function to determine if a propositional formula in conjunction normal form is a tautology. The algorithm you should and must use is a simple one:
• A disjunction of literals, a clause, is a tautology exactly when it contains both P and not P, for some proposition P.
• A conjunction is a tautology precisely when each conjunct is a tautology.

### Input

The program should get its input from the standard input stream. The input is any number of lines of US-ASCII text. Each line is a legal postfix expression representing a propositional formula. The only characters on the line are US-ASCII uppercase letters and spaces (which are ignored). Your program is not required to perform input validation.

The first column is the input, postfix character for the operators we consider (using Bocheński notation). Propositional names are single US-ASCII, uppercase letters not used as an operator (i.e., not ACDEJKN), typically 'P', 'Q', 'R', 'S' and so on.

 A v disjunction C => implication D | nand E <=> equivalence J + xor K & conjunction N ˜ unary negation

The second column is the string of US-ASCII characters used in the output. Note, however, that not all operators appear in the output.

Sample input:

```P                    P
PQRAKPQKC            ((P & (Q v R)) => (P & Q))
PQRAKPQKPRKAE        ((P & (Q v R)) <=> ((P & Q) v (P & R)))
```
The comments on the right are not part of the input and for informational purpose only.

### Output

For every line on input write two things to the standard output stream.
1. The word 'true' if the input is a tautology, or 'false' otherwise.
2. The input formula in conjunction normal form without simplification. All binary operators fully should be fully parenthesized and surrounded by spaces. (See the example below.)

It is quite likely that different programs will have different (but equivalent) output.

The output for the sample input shown above is as follows:

```false P
false ((((~P v ~Q) v P) & ((~P v ~R) v P)) & (((~P v ~Q) v Q) & ((~P v ~R) v Q)))
true  ((((((~P v ~Q) v (P v P)) & ((~P v ~Q) v (Q v P))) & (((~P v ~Q) v (P v R)) & ((~P v ~Q) v (Q v R)))) & ((((~P v ~R) v (P v P)) & ((~P v ~R) v (Q v P))) & (((~P v ~R) v (P v R)) & ((~P v ~R) v (Q v R))))) & ((((~P v ~Q) v P) & ((~P v ~R) v P)) & (((~P v ~Q) v (Q v R)) & ((~P v ~R) v (Q v R)))))
```

## Information on the net

Be sure to eliminate all warnings detected by -Wall before submitting your project. Do not use the do construct, records, or \$. Prove you know the basics by using the more common constructs, otherwise one might assume you are mimicking other Haskell code you do not understand.

## Turning it in

Usually, the file should be named after the module name, replacing dots in the module name by directory separators. For example, on a Unix system, the module A.B.C should be placed in the file A/B/C.hs, relative to some base directory. If the module is not going to be imported by another module (Main, for example), then you are free to use any filename for it.

Turn in the source code for your project in a file named Main.hs. Your project will be compiled like this:

```ghc -Wall --make Main.hs
```

Write the program as clearly as possible, including reasonable comments. You may work alone or with one other student in the class, as long as you did not work with this partner in any of the previous projects. If working together, have one person turn in the project

It is important to get the output formatted correctly, as the output must conform character by character to the specification. Incorrectly formatted output will fail the test cases. If there is any question about the output, please ask.

Turn in the Haskell source code for the program using the Submit Server. The project tag is proj4. In the comments somewhere at the beginning of your source file include a header like the following:

```{-