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

Project 4:


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:


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.


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:

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