CSE3001: ML Project

Due: 2002

Tautology Checker

In this project you are to to check if a propositional formula is a tautology. You need to write three ML functions:

nnf : formula -> formula
cnf : formula -> formula
checker : formual -> bool

Propositional Logic

Propositional logic deals with propositions constructed from atoms by the connectives "and", "or" and "not". A propositional formula may be

~p       "not p"
p &  q   "p and q"
p \/ q   "p or q"

Propositional formulas resemble boolean expressions and are represented in this project by the datatype formula:

datatype formula =
  Atom of string | Neg of formula | Disj of formula * formula | Conj of formula * formula

Put this datatype declaration exactly as it is in the beginning of your program. The implication p->q is equivalent to (~p)\/q.

A propositional formula is either true or false depending on the truth values of the constituent atomic propositions. So if P is true and Q is false, then

P     Q     ~ (P \/ Q)
=====================
T     F          F

A tautology is a propositional formula that is true regardless of the values of the atomic propositions. The formula ~ (P \/ Q) \/ P \/ Q is a tautulogy as seen by looking at its truth table.

P     Q     ~ (P \/ Q) \/ P \/ Q
================================
T     T                T
T     F                T
F     T                T
F     F                T

Negation Normal Form

Any proposition can be converted to negation normal form (NNF), where ~ is applied only to atoms, by pushing negation into the conjunctions and disjunctions. Repeatedly replace

~~p       by p
~(p & q)  by (~p) \/ (~q)
~(p \/ q) by (~p) &  (~q)

Such replacements are sometimes called rewrite rules.

Conjunction Normal Form

A literal is an atom or its negation. A proposition is in conjunctive normal form (CNF) if it has the form p1 & ... & pn where each pi is a disjunction of literals. To obtain CNF, start with a propositional formula in negation normal form. Using the the distributive law, push in disjunctions until they apply only to literals. In otherwords, repeadly replace

p \/ (q & r)   by  (p \/ q) & (p \/ r)
(q & r) \/ p   by  (q \/ p) & (r \/ p)

Tautology checking

To check whether a propositional formula p is a tuatology, reduce it to CNF, say p₁ & ... & p_n. If p is a tautology, then so is each p_i. Supppose the conjunct p_i is q1 \/ ... \/ qm where each qi is a literal. If the literals include an atom and its negation, then p_i is a tautology. If they do not, then p_i is not a tautology.

For example, the propositional formula A \/ B is not a tautology because:

A \/ B
A \/ B    (negation normal form)
A \/ B    (conjunctive normal form, one conjunct)

Since some conjunct, namely A\/B, does not contain any atom and its negation, the proposition A \/ B is not a tautology. So applying the ML program to this propositonal formula

checker (Disj (Atom "A", Atom "B"))

yields false.

For example, the propositional formula ~(A \/ B) is not a tautology because:

~ (A \/ B)
~A & ~B    (negation normal form)
~A & ~B    (conjunctive normal form, two conjuncts)

Since some conjunct (in fact both), does not contain any atom and its negation, the proposition ~(A \/ B) is not a tautology. So applying the ML program to this propositional formula

checker (Neg (Disj (Atom "A", Atom "B")))

yields false.

For example, the proposition A \/ ~((A & ~B) \/ (~C & C)) is a tautology because:

A \/ ~((A & ~B) \/ (~C & C))
A \/ ((~A \/ B) & (C \/ ~C))    (negation normal form)
A \/ ~A \/ B  &  A \/ C \/ ~C   (conjunctive normal form, two conjuncts)

Since all conjuncts contain an atom and its negation, the proposition is a tautology. So applying the ML program to this propositional formula

checker (
   Disj (
     Atom "A",
     Neg (
       Disj (
          Conj (Atom "A", Neg (Atom "B")),
          Conj (Neg (Atom "C"), Atom "C"))
       )
   )
)

yields true.

References

Information about propositional logic can be obtained from several discrete mathematics textbooks:

Daniel J. Velleman, How To Prove It: A Structured Approach, Cambridge University Press, Cambridge, England, 1994.

Chapter 1. Sentential Logic. Section 1.1. Deductive Reasoning and Logical Connectives, pages 7-13. Section 1.2. Truth Tables, pages 13-24.
Ralph P. Gimaldi, Discrete and Combinatorial Mathematics: An Applied Introduction, 3rd edition, Addison Wesley, Reading, Massachusetts, 1992.

Chapter 2. Fundamentals of Logic. Section 2.1. Basic Connective and Truth Tables, pages 51-60. Section 2.2. Logical Implication: The Laws of Logic, pages 60-76.

Information on the net

Turning it in

Turn in the file checker.sml that contains the source for the function checker.

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 any of them in the previous projects. Be sure to include your name and your partner's names in the comments when you turn in the project, so we will know who should get credit for the work. Use the following command on

-Dclass=cse3001 -Dproject=proj4

You can submit the project as often as you wish, as long as it is submitted from the same computer account, only the last one will be graded. Put your name or names in comments at the beginning of your program. You may wish to put your e-mail address in your program. Please, do not put your student number in any program.

Ryan Stansifer <ryan@cs.fit.edu>

Last modified: Sun Dec 8 17:36:25 EST 2002