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

Project 4:

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 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.

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)))

Output

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

• All things Haskell
• A Tour of the Haskell Syntax by Arjan van IJzendoorn
• A Tour of the Haskell Prelude, the most useful Haskell predefined functions
• Haskell Homework Help
• Good Haskell Style
• Study these main programs to see how to use the Haskell program interact. Think of a Haskell program as a function from the standard input stream (a string) to the standard output stream (a string).

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:

{-
 - Author: name1, e-mail address
 - Author: name2, e-mail address
 - Course: CSE 4250, Fall 2021
 - Project: Proj4, Tautology Checker
 - Language implementation: Glorious Glasgow Haskell Compilation System, version 8.4.3
 -}

It is expected that your program is well documented, conforms to widely accepted standards of style for Haskell, and terminates normally (in particular, does not call exit with non-zero status).

All programs are analyzed for similarity with other programs, both current and past. Students whose programs are very similar to other sources will receive no credit. This policy is necessary to ensure that students take reasonable action to avoid and prevent plagiarism, and to ensure the proper recognition of independent effort. Without student cooperation individual grades would have less meaning and the incentive for learning decreases. If you have evidence of academic misconduct, you should bring it to the attention of your instructor, the head of the department, or Dean of the school of engineering.