Encoding logic in AI using Theorem Proving
Tags: machinelearning, python
Published: 2020-07-07 10:12:31

_This article was originally posted on [Medium](https://medium.com/mindpload/encoding-logic-in-ai-using-theorem-proving-f20b3a980f67)_ and [Asheux](https://www.asheux.com/articles/4)

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/mqu79cw0klnmi96egxhp.jpg)

In my previous article on [knowledge representation using propositional logic](https://medium.com/mindpload/knowledge-representation-in-ai-a82c1f753746), we looked at a simple algorithm called _**model-checking**_ to show how to determine entailment in all possible worlds. Here, we draw our attention to a more efficient way to achieve the same goal by using _**theorem proving**_, the idea of applying _**inference rules**_ directly to the sentences in our knowledge base to develop a proof without ever requiring to enumerate models.

###### Inference rules

Proofs in mathematics are valid arguments that establish the truth of the desired goal. Therefore, inference rules are functions for building valid arguments. They take the premises, analyses their syntax and returns a conclusion.

***Basic concepts:***

* ≡: The equivalence connective
* Logical equivalence: two sentences are logically equivalence if they are true in the same set of possible models
* An argument is a sequence of sentences that end with a conclusion
* The validity of the argument is determined by the conclusion and the premises(preceding sentences). If the conclusion follows from the truth of the premises, then the argument is valid.

These rules are;

1. Modus ponens
2. And-Elimination
3. De Morgan's law
4. Double negation elimination
5. Implication elimination
6. Bi-conditional elimination
7. Distributive property

We will use the following structure to represent our inference rules, the line separates the premises and the conclusion.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/0a85011r684bm5nf4c99.png)

Let's look at each of these rules with some examples;

###### *Modus ponens*

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/9gczcc0ndsyho938fe5j.png)

The way to interpret this is, if we have access to some piece of information, α ⇒ β and we know that α is true then the conclusion we reach is β is true. Example;

```
           |
Premises   |     α ⇒ β: If Rey was free, then Rey would visit Ben
           |         α: Rey is free
           |
-----------|------------------------------------------------------
           |
Conclusion |         β: Rey would visit Ben
           |
```

###### *And-Elimination*

This states that from a conjunction (a sentence whose connective is ∧), any of the conjuncts (sentences connected by ∧) can be inferred:

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/lwszq77ebh15tm21tzll.png)

Example;

```
           |
Premises   |     α ∧ β: Rey is free on Wednesday and Friday
           |
-----------|------------------------------------------------
           |
Conclusion |         β: Rey is free on Friday
           |
```

###### _De Morgan's rule_

¬(α ∧ β) ≡ (¬α ∨ ¬β), De Morgan(∧)
¬(α ∨ β) ≡ (¬α ∧ ¬β), De Morgan(∨)

Using And(∧);

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/58fh30klpcordkz92p88.png)

Example;

```
           |
Premises   |     ¬(α ∧ β): Rey is not free on Wednesday and Friday
           |
-----------|------------------------------------------------------
           |
Conclusion |    (¬α ∨ ¬β): Rey is not free on Wednesday or Rey 
           |               is not free on Friday
           |
```

Using Or(∨)

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/aaxlodwwfo8tvmopncfb.png)

Example;

```
           |
Premises   |     ¬(α ∨ β): Rey is not free on Wednesday or Friday
           |
-----------|-----------------------------------------------------
           |
Conclusion |    (¬α ∧ ¬β): Rey is not free on Wednesday and Rey 
           |               is not free on Friday
           |
```

###### _Double negation elimination_

¬(¬α) ≡ α, double-negation elimination

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/8qf1wr36tbfo2ylkau67.png)

Example;

```
           |
Premises   |     ¬(¬α): It is not true that Rey did not succeed
           |
-----------|---------------------------------------------------
           |
Conclusion |         α: Rey succeeded
           |
```

###### _Implication elimination_

(α ⇒ β) ≡ (¬α ∨ β), implication elimination

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/0x3ej7ljiwx2yntozovj.png)

Example;

```
           |
Premises   |     (α ⇒ β): If Rey was free, then Rey would visit Ben
           |
-----------|------------------------------------------------------
           |
Conclusion |    (¬α ∨ β): Rey is not free or Rey would visit Ben
           |
```

The way to think about this rule is, given an if-then statement,

(α ⇒ β): If Rey was free, then Rey would visit Ben

we can translate it to an or statement by making the if statement false or true. For example; The conclusion could be Rey is not free or Rey is free(¬α ∨ α). But we know when Rey is free(α), she would visit Ben(β). Therefore, we replace α with β in our inference(¬α ∨ α) to make the final conclusion that Rey is not free or Rey would visit Ben(¬α ∨ β).

###### _Bi-conditional elimination_

(α ⇔ β) ≡ ((α ⇒ β) ∧ (β ⇒ α)), bi-conditional elimination

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/lke6gkax9au5gnjzto8x.png)

The premise here can be translated as 'α if and only if β'. Example;

```
           |
Premises   |     (α ⇔ β): Rey is free if and only if it's Monday
           |
-----------|------------------------------------------------------
           |
Conclusion |(α ⇒ β)∧(β ⇒ α): If Rey is free, then it is Monday
           |                 and if it is Monday, then Rey is free
```

###### _Distributive property_

(α ∧ (β ∨ γ)) ≡ ((α ∧ β) ∨ (α ∧ γ)), distributive of ∧ over ∨
(α ∨ (β ∧ γ)) ≡ ((α ∨ β) ∧ (α ∨ γ)), distributive of ∨ over ∧

Using And(∧) over Or(∨);

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/kjep0ij2ipopj00fj4v9.png)

Using Or(∨) over And(∧);

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/00qf0bqkn1fy97cjgo5r.png)

Now let's use these inference rules to draw some conclusion or proof that a query is true. Firstly, we define a proof problem as follows;

* Initial state: the beginning knowledge base
* Actions: All the inference rules
* Result or transition model: the new knowledge base
* Goal: The state containing the sentence we are trying to prove

###### Resolution rule

This is another type of inference rule that yields a complete inference algorithm.

Basic concepts;

* **Literals**: Propositional symbols or the negation of propositional symbols
* **Clause**: a dis-junction of **literals**

Let's see some examples to help us understand this rule;

Given the clause A = (P ∨ Q ∨ R) and the literal ¬P, using this rule, the literal ¬P resolves with P in A. This results to the clause B = ( Q ∨ R) as the re-solvent. This can be interpreted in simple terms as;

```
(P ∨ Q ∨ R): if Rey is in the house or Ben is sick or it is Wednesday

And we know that ¬P: Rey is not in the house; then we can conclude that;

(Q ∨ R): Ben is sick or it is Wednesday.
```

Here P and ¬P are **complimentary literals** or literals that cancel each other. And this is a type of resolution called **unit resolution** (takes in a clause and a literal and produces a new clause.

Note that the resulting clause or re-solvent should contain only one copy of each literal. For example given (P ∨ Q) and (¬P ∨ Q), we get (Q ∨ Q).

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/rxiq3wvem170v7tjki3e.png)

But we need the literals to be unique, so we perform a process called **factoring** on the resultant clause to factor out the literals appearing more than once. From the above example, we will have;

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/id2dhaoiff7gj1b7yg2h.png)

Now to determine the entailment of the sentence α and β in propositional logic we use resolution rule for knowledge bases expressed in **conjunctive normal form**(see below).

Conjunctive normal form(CNF)

The form in which a logical sentence is expressed as a conjunction of clauses leading to a complete inference procedure for all of propositional logic.
Conversion to CNF

* Eliminate bi-conditionals; turn (α ⇔ β) to (α ⇒ β) ∧ (β ⇒ α).
* Eliminate implication; turn (α ⇒ β) to ¬α ∨ β.
* Move the Not(¬) inwards by applying De Morgan's rule and double-negation elimination; ¬(α ∧ β) ≡ (¬α ∨ ¬β) and ¬(¬α) = α respectively.
* Use distributive law to distribute nested ∧ and ∨ operators applied to literals.

Example using sentence A ⇔ (B ∨ C);

_Bi-conditionals_

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/n8uyiz2g89u5vri05r36.png)

_Implication_

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/hlitbvlsan9qytlarmwm.png)

_De Morgan's rule_

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/ogkzxwof205ihs2e7ul8.png)

_Distributive law_

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/gqsxtu8ghl4o2vix5qbp.png)

The converted CNF is (¬A ∨ B ∨ C) ∧ (¬B ∨ A) ∧ (¬C ∨ A).

Point to note is, when you resolve a single sentence with it's negation, we might get an empty clause represented by **empty clause** = (). And the **empty clause** is always false. Example, P and ¬P gives = (), meaning it's is false.

###### _Resolution algorithm_

The idea of proof by contradiction is pretty famous in computer science; the idea that given a proposition, to determine it's validity or truth we first assume that the proposition to be false and show that it leads to a contradiction.

Applying this concept in resolution rule, we look at how to determine the truth of the sentence (KB |= α) (KB is the knowledge base). We start by assuming (¬α) and show that (KB ∧ ¬α) leads to a contradiction; if so, the sentence KB |= α is true, otherwise it is false. How?

_Procedure:_

1. Convert the sentence KB |= α to Conjunctive Normal Form(CNF)
2. Apply resolution rule to the resulting clauses to produce a new clause and keep doing this;

* If the produced clause is empty = () = false, there is a contradiction, therefore, KB |= α is true
* Otherwise, if we cannot add new clauses, KB |= α is false, hence, there is not entailment

Example;

Using the above CNF converted sentence.

```
CNF = R0 = (¬A ∨ B ∨ C) ∧ (¬B ∨ A) ∧ (¬C ∨ A)
```

We want to check that R0 entails the query A or (R0 |= A).

First thing is to assume our query is false. i.e ¬A. Then form the following sentence.

```
R1 = (¬A ∨ B ∨ C) ∧ (¬B ∨ A) ∧ (¬C ∨ A) ∧ ¬A
```

Then we show that R1 leads to a contradiction;

**Step 1**: Pick 2 clauses (¬A ∨ B ∨ C) and (¬B ∨ A), because they have complimentary literals, and resolve them;

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/kw6333rozznwucqod8uu.png)

Our new premise becomes, R2 below, ignoring the previous picked clauses;

```
R2 = (¬C ∨ A) ∧ ¬A
```

**Step 2**: Pick another clause to resolve that has literals which is complimentary to the new previously formed clause (C). i.e (¬C ∨ A).

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/lbxa0q82jmow9ounopae.png)

New premise;

```
R3 = (¬A)
```

**Step 3**: Since we only have one last clause, we resolve it.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/xgd8owe1ht7zbheun7d1.png)

Our resulting clause is an empty clause which means it is false. We then conclude based on proof by contradiction that there is a contradiction. Therefore, the sentence (R0 |= A) is true.

###### _Resolution programmatically_

_Pseudo-code:_

```
function RESOLUTION(KB, α) returns true or false
  inputs: KB, the knowledge base, a sentence in propositional logic
           α, the query, a sentence in propositional logic
  
  clauses ← the set of clauses in the CNF representation of KB ∧ ¬α
  new ← { }
  loop do
    for each pair of clauses C[i] , C[j] in clauses do
      resolvents ← RESOLVE(C[i], C[j])
      if resolvents contains the empty clause then
        return true
      new ← new ∪ resolvents
    if new ⊆ clauses then
      return false
    clauses ← clauses ∪ new
```

###### References

- [Introduction to Artificial Intelligence with Python](https://courses.edx.org/courses/course-v1:HarvardX+CS50AI+1T2020/course/)
- (Global Edition) Stuart J. Russell, Peter Norvig - Artificial Intelligence_ A Modern Approach, 3rd Edition-Pearson Education (2016), pg 234