# 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

1. Biconditional elimination
2. DeMorgan
3. Or-distribution
4. 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!