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!