Logical Normal Forms, Part 1

Due
Wed Oct 23 11:59 pm
Starter files
lab6.zip
Submission
Please submit your work using Gradescope.

Introduction

The goal of this two-part lab is to write software that takes a proposition and expresses it in conjunctive normal form (CNF).

Why is this important? In an earlier lab, we saw the value of writing propositions in CNF. It’s valuable because we can design algorithms that are specialized for the conjunctive normal form (e.g., SatSolver). This lab has practical value because now we can take anything expressed in propositional logic – e.g, the rules of the Paris Metro railway control system – and convert it into CNF for further processing.

Java representation of logical propositions. Similar what is described in the textbook (Ch 5.4), propositions are represented using a recursively defined structure (see the Proposition class and its subclasses). The structure forms a binary tree. Internal nodes represent logical operations – e.g., the proposition $\varphi := \alpha \land \beta$ is represented as a binary tree where the root of the tree represents the AND and the two subtrees are the propositions $\alpha$ and $\beta$. The leaves of the tree are atomic propositions – i.e., they are variables such as $p$, $q$, $r$, etc.

Converting to CNF. Transforming a proposition to CNF is done in stages. Each stage takes propostion and recursively manipulates it, producing a new proposition that is logically equivalent to the input proposition but in a desired form.

Given input proposition $\varphi$, the stages are:

  1. Simplify $\varphi$ so it only contains $\land$ and $\lnot$. We’ll call this “simplified” $\varphi$.
  2. Convert “simplified” $\varphi$ into negation normal form (NNF). We’ll call this “NNF” $\varphi$. (Note: this may introduce some $\lor$’s because of DeMorgan’s law.)
  3. Convert “NNF” $\varphi$ into CNF. The key idea here is to distribute $\lor$ over $\land$.

You are asked to implement methods for each of these stages. In part 1 of the lab, your task is to implement NormalForms.simplify and NormalForms.toNNF. In part 2, you will be asked to implement NormalForms.fromNNFtoCNF and NormalForms.toCNF.

Overview of Starter Code

You are expected to modify these files:

  • Neg.java – a propostion made up the negation of a proposition (e.g., $\lnot \alpha$).
  • NormalForms.java – methods that convert a proposition to a normal form
  • PropVariable.java – a proposition consisting of a single variable

You are expected to read, use, but not modify these files:

  • BinOp.java – a proposition made up of two proposition connected by a binary logical connective (e.g., $\alpha \land \beta$)
  • Proposition.java – an abstract class representing all propositions
  • Build.java – useful helper methods for writing complex propositions; also illustrates how the pieces come together.
  • LogicalConnective.java – the class representing the actual logical connectives $\land$, $\lor$, $\implies$, and $\lnot$.
  • IllegalPropositionException.java – the kind of exception you should throw if you encounter in an invalid input

Tasks

Here’s a rough guide on how to proceed.

  1. Browse the files, getting familiar with the code and and looking for “implement me!”, which is an indication that you are supposed to implement this function.
  2. Implement helper methods in Neg.java and Variable.java. Look at Proposition.java and BinOp.java for guidance.
  3. Implement NormalForms.simplify(). (You might find it helpful to consult Ch. 5.4 of the textbook.) You should find the helper methods in Proposition to be very useful here, e.g. Proposition.isVariable(). Use the main method in NormalForms to test your implementation.
  4. Implement NormalForms.toNNF(). Again, test your implementation.

Throughout, read the javadocs closely. For instance, the javadocs will tell you under what circumstances your code should throw an exception.