Propositional logic is a reasoning tool that deals with propositions. The very basic truth values in propositional logic are $true$ and $false$. An atomic proposition is represented by a symbol such as $p$ and $q$, we may further have negations of propositions, e.g., $\neg p$. By using logical connections such as conjunctions $\wedge$, disjunctions $\vee$, and implications $\rightarrow$, we can express complex propositions.

In this post, I will demonstrate some Racket programs that transform and reason propositional logics.

### Negation Normal Forms

The first program is the transformation to Negation Normal Forms (NNF). NNF allows negations appear only for literals, and the connections can be used in NNF are disjunctions $\vee$, conjunctions $\wedge$. So implications are not allowed. NNF forms the foundation of transforming to other forms such as Disjunctive Normal Forms (DNF) and Conjunctive Normal Forms (CNF).

The following Racket program `nnf`

does the transformation. The core idea is using the De Morgan’s Law:

$$ \neg (P \wedge Q) \leftrightarrow \neg P \vee \neg Q \text{ and }

\neg (P \vee Q) \leftrightarrow \neg P \wedge \neg Q $$

```
(define (nnf prop)
(match prop
['(¬ ⊤) '⊥]
['(¬ ⊥) '⊤]
[(? symbol? x) x]
[`(¬ ,(? symbol? x)) `(¬ ,x)]
[`(¬ (¬ ,p)) (nnf p)]
[`(¬ (,p → ,q)) (nnf `(¬ ((¬ ,p) ∨ ,q)))]
[`(¬ (,p ∧ ,q)) (nnf `((¬ ,p) ∨ (¬ ,q)))]
[`(¬ (,p ∨ ,q)) (nnf `((¬ ,p) ∧ (¬ ,q)))]
[`(,p → ,q) (nnf `((¬ ,p) ∨ ,q))]
[`(,p ∧ ,q) `(,(nnf p) ∧ ,(nnf q))]
[`(,p ∨ ,q) `(,(nnf p) ∨ ,(nnf q))]))
```

This is an example of NNF transformation:

```
(check-equal? (nnf '(¬ ((¬ (p ∧ q)) → (¬ r))))
'(((¬ p) ∨ (¬ q)) ∧ r))
```

### Disjunctive Normal Forms

Disjunctive Normal Forms are disjunctions of conjunctions. To transform a formula to DNF, we firstly transform it to NNF, and then apply the following rules to propagate conjunctions into disjunctions:

$$ (P \vee Q) \wedge R \leftrightarrow (P \wedge R) \vee (Q \wedge R) \text{ and }

P \wedge (Q \vee R) \leftrightarrow (P \wedge Q) \vee (P \wedge R) $$

The following code shows how to distribute conjunctions, and then compose `dnf/dist`

and `nnf`

to obtain `dnf`

.

```
(define (dnf/dist prop)
(match prop
[`((,p ∨ ,q) ∧ ,r) `(,(dnf/dist `(,p ∧ ,r)) ∨ ,(dnf/dist `(,q ∧ ,r)))]
[`(,p ∧ (,q ∨ ,r)) `(,(dnf/dist `(,p ∧ ,q)) ∨ ,(dnf/dist `(,p ∧ ,r)))]
[p p]))
(define dnf (compose dnf/dist nnf))
```

An example of DNF Transformation:

```
(check-equal? (dnf '((Q1 ∨ (¬ (¬ Q2))) ∧ ((¬ R1) → R2)))
'(((Q1 ∧ R1) ∨ (Q1 ∧ R2)) ∨ ((Q2 ∧ R1) ∨ (Q2 ∧ R2))))
```

### Conjunctive Normal Forms

Conjunctive Normal Forms are conjunctions of disjunctions. To transform a formula to CNF, we firstly transform it to NNF, and then apply the following rules to propagate disjunctions into conjunctions:

$$ (P \wedge Q) \vee R \leftrightarrow (P \vee R) \wedge (Q \vee R) \text{ and }

P \vee (Q \wedge R) \leftrightarrow (P \vee Q) \wedge (P \vee R) $$

The following code show how to distribute conjunctions, and then compose `dnf/dist`

and `nnf`

to obtain `dnf`

.

```
(define (cnf/dist prop)
(match prop
[`((,p ∧ ,q) ∨ ,r) `(,(cnf/dist `(,p ∨ ,r)) ∧ ,(cnf/dist `(,q ∨ ,r)))]
[`(,p ∨ (,q ∧ ,r)) `(,(cnf/dist `(,p ∨ ,q)) ∧ ,(cnf/dist `(,p ∨ ,r)))]
[p p]))
(define cnf (compose cnf/dist nnf))
```

An example of CNF Transformation:

```
(check-equal? (cnf '((Q1 ∧ (¬ (¬ Q2))) ∨ ((¬ R1) → R2)))
'((Q1 ∨ (R1 ∨ R2)) ∧ (Q2 ∨ (R1 ∨ R2))))
```

### Validity Checking

A propositional formula $F$ is valid iff $F$ is true under all interpretations. An interpretation is a set of assignments of symbols in the formula. Formally speaking, $F$ is valid $\Leftrightarrow$ $\forall I . I \models F$. We can check the validity of a formula by enumerating all possible assignments, this method is called *truth table methods*. But it is computational inefficient: if there are $n$ symbols in the formula, then we need to check $2^{n}$ assignments, which is intractble.

An approach of checking validity is *semantic argument method*. The idea behind it is, given a formula $F$, we firstly assume that $F$ is invalid (i.e., exists at least one interpretations that makes $F$ to be false), then we can apply some deduction rules (according to the semantics) to deduce some facts recursively until we can not do so. If there are two deduced facts are contradictory, then we know the assumption can not be true. But note that there are possibly many proof branches; to show the validity, we must derive contradictions at every proof branch.

We first define some data structure to represent logical consequence and its negation. We also define `And`

, `Or`

, and `None`

to represent the fact we can deduce from a given proposition.

```
(struct ⊨ (formula) #:transparent)
(struct ⊭ (formula) #:transparent)
(struct And (fs) #:transparent)
(struct Or (fs) #:transparent)
(struct None () #:transparent)
(define (deduce asmp)
(match asmp
[(⊨ `(¬ ,p)) (And (list (⊭ p)))]
[(⊭ `(¬ ,p)) (And (list (⊨ p)))]
[(⊨ `(,p ∧ ,q)) (And (list (⊨ p) (⊨ q)))]
[(⊭ `(,p ∧ ,q)) (Or (list (⊭ p) (⊭ q)))]
[(⊨ `(,p ∨ ,q)) (Or (list (⊨ p) (⊨ q)))]
[(⊭ `(,p ∨ ,q)) (And (list (⊭ p) (⊭ q)))]
[(⊨ `(,p → ,q)) (Or (list (⊭ p) (⊨ q)))]
[(⊭ `(,p → ,q)) (And (list (⊨ p) (⊭ q)))]
[(⊨ `(,p ↔ ,q)) (Or (list (⊨ `(,p ∧ ,q)) (⊭ `(,p ∨ ,q))))]
[(⊭ `(,p ↔ ,q)) (Or (list (⊨ `(,p ∧ (¬ ,q))) (⊨ `((¬ ,p) ∧ ,q))))]
[p (None)]))
```

The function `deduce`

generates the facts that we may infer given a proposition. The facts are represented by either `And`

or `Or`

, the former one requires all propositions in it must be hold, and the later one just requires at least one holds.

```
(define (contradict? p asmps)
(match asmps
[(list) #f]
[(list q rest ...)
(match* (p q)
[((⊨ f) (⊭ f)) #t]
[((⊭ f) (⊨ f)) #t]
[(_ _) (contradict? p rest)])]))
```

The function `contradict?`

checks whether a proposition is contradicted with the given set of assumptions `asmps`

.

```
(define (valid? p)
(define asmp (⊭ p))
(define (valid/aux? worklist asmps)
(match worklist
[(list) #f]
[(list q rest ...)
(if (contradict? q asmps) #t
(match (deduce q)
[(And fs) (valid/aux? (append fs rest) (append fs asmps))]
[(Or fs) (foldl (λ (f b) (and b (valid/aux? (cons f rest) (cons f asmps)))) #t fs)]
[(None) (valid/aux? rest asmps)]))]))
(valid/aux? (list asmp) (list asmp)))
```

The function `valid?`

checks the validity. We use a worklist which represents the deduced facts that should hold. In the `Or`

case, we have multiple proof branches, and we need to check that a contradiction exists for every branch, thus a `foldl`

is used.

Some examples of valid and invalid formulas:

```
(check-true (valid? '((A → B) ↔ ((¬ B) → (¬ A)))))
(check-true (valid? '((((¬ A) → B) ∧ ((¬ A) → (¬ B))) → A)))
(check-true (valid? '((¬ (A ∧ B)) ↔ ((¬ A) ∨ (¬ B)))))
(check-true (valid? '(C → C)))
(check-true (valid? '((A ∨ B) → (A ∨ B))))
(check-false (valid? '((P → (Q → R)) → ((¬ R) → ((¬ Q) → (¬ P))))))
```

### Tseitin Transformation

The CNF transformation we just showed correctly does the job, but the size of the generated formula is exponentially large than the original one. An algorithm called Tseitin transformation generates CNF formula in linear size of the original one. The following program implements Tseitin transformation:

```
(define (subformulae f)
(set-union
(set f)
(match f
[(? symbol? x) (set)]
[`(¬ ,x) (set-union (subformulae x))]
[`(,p ∧ ,q) (set-union (subformulae p) (subformulae q))]
[`(,p ∨ ,q) (set-union (subformulae p) (subformulae q))]
[`(,p → ,q) (set-union (subformulae p) (subformulae q))]
[`(,p ↔ ,q) (set-union (subformulae p) (subformulae q))])))
(define (formula->string f)
(match f
[(? symbol? x) (symbol->string x)]
[`(¬ ,x) (string-append "¬" (formula->string x))]
[`(,p ∧ ,q) (string-append "<" (formula->string p) " ∧ " (formula->string q) ">")]
[`(,p ∨ ,q) (string-append "<" (formula->string p) " ∨ " (formula->string q) ">")]
[`(,p → ,q) (string-append "<" (formula->string p) " → " (formula->string q) ">")]
[`(,p ↔ ,q) (string-append "<" (formula->string p) " ↔ " (formula->string q) ">")]))
(define (rep f)
(match f
['⊤ '⊤] ['⊥ '⊥]
[(? symbol? x) x]
[else (string->symbol (string-append "ϕ" (formula->string f)))]))
(define (encode f)
(define p (rep f))
(match f
['⊤ '⊤] ['⊥ '⊥]
[(? symbol? x) '⊤]
[`(¬ ,f) `(((¬ ,p) ∨ (¬ ,(rep f))) ∧ (,p ∨ ,(rep f)))]
[`(,f1 ∧ ,f2)
`(((¬ ,p) ∨ ,(rep f1)) ∧
((¬ ,p) ∨ ,(rep f2)) ∧
((¬ ,(rep f1)) ∨ (¬ ,(rep f2)) ∨ ,p))]
[`(,f1 ∨ ,f2)
`(((¬ ,p) ∨ ,(rep f1) ∨ ,(rep f2)) ∧
((¬ ,(rep f1)) ∨ ,p) ∧
((¬ ,(rep f2)) ∨ ,p))]
[`(,f1 → ,f2)
`(((¬ ,p) ∨ (¬ ,(rep f1)) ∨ ,(rep f2)) ∧
(,(rep f1) ∨ ,p) ∧
((¬ ,(rep f2)) ∨ ,p))]
[`(,f1 ↔ ,f2)
`(((¬ ,p) ∨ (¬ ,(rep f1)) ∨ ,(rep f2)) ∧
((¬ ,p) ∨ ,(rep f1) ∨ (¬ ,(rep f2))) ∧
(,p ∨ (¬ ,(rep f1)) ∨ (¬ ,(rep f2))) ∧
(,p ∨ ,(rep f1) ∨ ,(rep f2)))]))
(define (all-but-last lst) (reverse (rest (reverse lst))))
(define (cnf/simplify f)
(match f
[`(,p ∧ ⊤) `(,p)]
[`(⊤ ∧ ,rest ...) (cnf/simplify rest)]
[`(,p ∧ ,rest ...) `(,p ∧ ,@(cnf/simplify rest))]
[else f]))
(define (tseitin f)
(define ensf (map encode (set->list (subformulae f))))
(define conj/ensf (foldr (λ (f all)
(if (list? f) `(,@f ∧ ,@all) `(,f ∧ ,@all)))
(last ensf) (all-but-last ensf)))
(cnf/simplify `(,(rep f) ∧ ,@conj/ensf)))
```