# Propositional logic theorem prover

## Introduction

We often think AI as moving a robot in our world. But AI is defined as the ability for the computer to do smart choices. It can be used in a system to anticipate user's actions and prepare a cache to improve speed ; used to do smart advertisement etc.

Today, we will study an agent able to learn using logical rules. We give our agent a little (but consistent) knowledge base and our agent will use logical deduction to "discover" its world. For instance, an agent knowing

```
A ⇒ B
B ⇒ C
```

is true, is able to deduce `B`

(if `B`

was false, there will be a contradiction with the knowledge base, assumed to be true)

## Propositional Logic

### Syntax

```
Literal = [a-zA-Z]+
Sentence = ~Sentence
| '(' Sentence ')'
| '[' Sentence ']'
| Sentence Op Sentence
| '¬' Sentence
| Sentence
Op = '⇒' | '⇔' | '∧' | '∨'
```

### Rules

We will define a basis for rewriting a propositional sentence. These rules will be used in the next part: solving.

```
Biconditional elimination: A ⇔ B = (A ⇒ B) ∧ (B ⇒ A)
Implication elimination: A ⇒ B = ¬A ∨ B
De Morgan (1): ¬(A ∨ B) = ¬A ∧ ¬B
De Morgan (2): ¬(A ∧ B) = ¬A ∨ ¬B
Distributivity (1): (A ∧ B) ∨ C = (A ∨ C) ∧ (B ∨ C)
Distributivity (2): (B ∨ C) ∧ A = (A ∧ C) ∨ (B ∧ C)
Double Negation: ¬¬A = A
```

### CNF Sentence

Using these rules, we can change any propositional sentence into a CNF sentence, a **Conjunctive Normal Form** is a set of clauses, interpreted as a conjunction. For instance:

`{A ∨ B, ¬B} = (A ∨ B)`

And we can represent the conjunction as a set too.

`{{A, B}, {¬B}} = {A ∨ B, ¬B} = (A ∨ B)`

This is easy to treat this form with algorithms

### Tautology

A tautology is a sentence wich is always true. The simplest tautology is:

`¬A ∨ A`

## Theorem Proving

We will prove theorems using reduction to absurdity: given a knowledge base `KB`

, we want to know if `KB ⇒ P`

for any sentence `P`

. `KB ⇒ P`

is equivalent to `KB ∧ ¬P`

. And all we have to do is to entail from what we know since a contradiction is found or nothing can be entailed, and no contradiction can exist.

### To CNF

To convert to CNF Sentence, you have to

- Biconditional elimination
- DeMorgan
- Or-distribution
- Converting to a set of sets

```
toCNF :: Logic -> [[Logic]]
toCNF = cnf . distribute . deMorgan . bicondElim
```

### Resolution rule

The most important theorem in theorem proving is the resolution rule: Given two CNF sentences, if a sentence contains a term negated in the other sentence, we can produce a resulting sentence, union of both, without these two terms. One at a time.

### Solve

We can write the algorithm to look for a contradiction

```
Entails(clauses) : Bool
new <- {} // new will be the set containing entailed sentence
forever
foreach pair of clauses Ci, Cj in clauses
resolvents <- Resolve(Ci, Cj)
if resolvents contains the empty clause
return true // We found a contradiction
if resolvents is not a tautology
new <- new Union resolvents
if new is subset of clauses
return false
Resolve(Ci, Cj) : Sentence
Ci <- Ci without redundancy
Cj <- Cj without redundancy
return ResolutionRule(Ci Union Cj)
```

And now, using your imagination, you can build a logical agent!