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!