Knowledge Representation

Let us again consider the MopBot example. Remember, our MopBot has:

• Sensors, which enables it to detect whether there is dirt in the room.
• Actuators, which enables it to clean the room or move to another room.

Suppose we want to tell that MopBot should clean room B and come back to room A. It might develop the following simple plan \(p_1\) to achieve the goal:

1. Move to B.
2. Clean B.
3. Leave B when no dirt is detected.

Alternatively, the MopBot may also adopt a more complex plan \(p_2\) to achieve the goal:

1. Move to B.
2. If dirt is detected, clean B. Otherwise, there is no need to clean.
3. Leave B when no dirt is detected.

Here, MopBot had known two things:

• No dirt is detected when the room is clean.
• Leave room B when no dirt is detected.

From the above two statements, we want MopBot to have knowledge of leave room B when the room is clean; in other words, we want MopBot to somehow store this knowledge.

10.1 Propositional logic

Knowledge is a concept that is very hard to define, but one definition of knowledge that has been generally agreed upon is: An agent A knows that statement S is true if and only if:

1. S is true.
2. A believes S is true.
3. A is justified in believing that S is true.

$~~~~$We will now introduce the idea of \(propositions\), which are variables that take on values \(True\) or \(False\). We can decide whether or not we can make such deductions by replacing these statements with propositions. For instance, assume

• \(g\) represent Greeks,
• \(h\) represent Humans,
• \(m\) represent Mortals.

$~~~~$The problem is, in general, we can not differentiate between whether statement S is true or Agent A believes that S is true. With the statements “all Greeks are human” and “all humans are mortal”, we can deduce that “all Greeks are mortal”. However, with “not all Greeks are human” and “all humans are mortal”, we are not able to deduce that “not all Greeks are mortal”.

$~~~~$After introducing propositions, we need a way of combining them to construct meaningful sentences. This led to the introduction of operators, including:

• unary operators: $¬$ (Negation)
• binary operations: $∧$ and $∨$, $a→b≡¬a∨b$

Finally, we would want to be able to express our knowledge base (\(KB\)). The language of knowledge base:

• \(PROP\): the set of all propositions, and
• \(FORM\): the set of all formulas/sentences that can be expressed by propositional logic.

Using these expressions, we will be able to classify which statements are allowed in propositional logic and which are not allowed. For instance, \((p ∨ q)\) is allowed under \(PROP\) and \(FORM\), whereas \((p ∧ q)\) is not allowed. \(FORM\) can be recursively defined as such:

\(~~~~~~~~~~FORM_0 = PROP\)
\(~~~~~~FORM_{i+1} = FORM_i ∪ \{(α ◦ β)|α, β ∈ FORM_i\} ∪ \{(¬α)|α ∈ FORM_i\}\) \(~~~~~~~~~~~~FORM = \bigcup\limits_{i=0}^{\infty} FORM_i\)

where \(α ◦ β ≡ \{(α ∨ β)\} ∨ \{(α ∧ β)\}\). Every \(α ∈ KB\) is also in \(FORM\).
$~~~~$Every formula \(φ\) may be true or false depending on the situation. For example: \(p ∨ q\) is true when \(p=0\) and \(q=1\), but false when \(p=0\), \(q=0\). Here, we define the notion of truth assignment \(τ\).

If a formula \(φ\) is true in \(τ\), we say \(τ \models φ\). To check whether \(τ \models φ\) or not, we can substitute every propositional variables with its truth value, and if \(φ\) evaluates to true then \(τ \models φ\) else not.

where \(φ(τ)\) is \(φ\) after substituting propositions of \(φ\) with their values in \(τ\).

Let us consider an example to understand the aforementioned statement. \(~~~~φ=((p ∨q)∧(¬r))\)
\(~~~~τ_1 =\{p→1,q→1,r→1\} ~~~~~~~~~~~~~~~~~~~~~~~~~ φ(τ_1)=0 ~~~~~~~~~~~~~~~~~~~~~~~~~ τ_1 \not\modelsφ\)
\(~~~~τ_2 =\{p→1,q→0,r→0\} ~~~~~~~~~~~~~~~~~~~~~~~~~ φ(τ_2)=1 ~~~~~~~~~~~~~~~~~~~~~~~~~ τ_2 \models φ\)

There are \(2^{\vert PROP \vert}\) possible truth assignments.

• \(φ\) is SAT (Satisfiable): \(∃τ\) such that \(τ \models φ\).
• \(φ\) is Valid: \(∀τ, τ \models φ\).
• \(φ\) is UNSAT (Unsatisfiable): \(∀τ,τ \not\models φ\) or there does not exist \(τ\) such that \(τ \models φ\).
• One important observation: \(φ\) is valid iff \(¬φ\) is UNSAT.

A few examples to understand the above definitions.

• \((p ∨ ¬p)\) is valid and SAT.
• \((p ∨ q)\) is SAT, but not valid.
• \((p∨q)∧(¬p∨q)∧(p∨¬q)∧(¬p∨¬q)\) is UNSAT.

$~~~~$This allows us to find meanings in the sentences; for example, \((p ∨ q)\) and \((q ∨ p)\) are different strings but seem to have meanings. In general, two formulas \(φ\) and \(Φ\) are called semantically equivalent \((φ ↔ Φ)\) if the following holds:

Some definitions:

• $ψ\models φ$ iff $ψ→φ$ is valid.
• $ψ\equiv φ$ iff $ψ↔φ$ is valid.
• If $ψ\equiv φ$, then \(φ\) and \(ψ\) are called semantically equivalent.

$~~~~$For example: let \(φ = (p ∨ (q ∧ r))\) and \(Φ = ((p ∨ q) ∧ r)\). \(φ \not\leftrightarrow Φ\) as for \(τ = \{p → 1, q → 1, r → 0\}\), \(φ(τ)\ne ψ(τ)\). Similarly:

Where \(C_1, C_2, C_3, C_4 ∈ FORM\). Essentially, the position of parenthesis does not matter when all \(C_i\)’s are connected with \(∧\); in that case, we are going to simply pretend that parenthesis does not exist.

10.2 Conjunctive Normal Form (CNF)

Where every \(Clause ~ C_i\) is expressed as disjunction of \(Literals\).
\(C_i =(l_{1_i} ∨l_{2_i} ∨...∨l_{k_i})\) where \(l_{j_i} ∈ \{p\vert p∈PROP\}∪\{¬p\vert p∈PROP\}\). For example:

\(~~~~~~~~~~C_1 :(p∨q∨¬r)\)
\(~~~~~~~~~~C_2 :(q∨¬s∨r)\)
\(~~~~~~~~~~C_3 :(p∨¬q∨s)\)
\(~~~~~~~~~~~~φ:C_1 ∧C_2 ∧C_3\)

Clauses: $C_1,C_2,C_3$, literals: $p,\lnot p, q, \lnot q, r, \lnot r, s, \lnot s$.

By applying simple distribution of $\lor$, and $\land$, we can convert any formula into CNF. For example:

Theorem 1 Every Formula $\varphi$ can be converted into CNF, say $\varphi_{CNF}$.

Now, let us go back to our classification of formula being SAT or UNSAT. The important question here is, how to find if a formula $\varphi$ is SAT or UNSAT. The naive approach can be to simply go over every possible truth assignment $\tau$, and check if $\varphi(\tau)=$ TRUE or FALSE. But, this approach will not work, if the formula is too large; let $\varphi = p_1 \land \lnot p_1 \land (p_2 \lor p_3 \lor p_4) \land \ldots$ with \(PROP = \{p_1,\ldots,p_{1000}\}\), is $\varphi$ SAT or UNSAT ? As we know $p_1 \land \lnot p_1 \to \square $, the formula $\varphi$ is UNSAT. $\square$ represents the placeholder for UNSAT.

10.3 Resolution Refutation

Let us consider a statement $\varphi = (\alpha \vee p) \wedge (\neg p \vee \beta)$. Next, using a truth table, it can be shown that \(\varphi \rightarrow (\alpha \vee \beta)\)

Therefore, as seen from Table 1,

Observe that if $C_1 \wedge C_2 \rightarrow C_3 \mbox{ is valid then } C_1 \wedge C_2 \leftrightarrow C_1 \wedge C_2 \wedge C_3$ Therefore,

Thus, to prove that a formula given in CNF is UNSAT, we can repeatedly apply resolution until a contradiction (e.g. $~$$p \wedge \neg p$) is reached.

Example of Resolution to Prove UNSAT

Consider the following statement in CNF.

Denote each clause by $C_i$, where $i$ is the order in which the clause appears in the statement. In other words, the statement is equivalent to $C_1 \wedge C_2 \wedge \cdots \wedge C_6$.

Resolve $C_1$ and $C_2$:

Resolve $C_7$ and $C_3$:

Resolve $C_8$ and $C_4$:

Resolve $C_5$ and $C_6$:

Resolve $C_9$ and $C_{10}$:

Definition 1 A resolution refutation of a formula $\varphi$ given in CNF, is a list of clauses $C_1,C_2, \cdots, C_t$ such that either $C_i \in \varphi$ or $C_i$ is derived from $C_a, C_b$ using resolution where $a,b<i$, and the last clause $C_t= \square$.

In the previous example, the resolution refutation is the list of clauses $C_1,C_2,C_3,\cdots, C_{10}, C_{11}$, where $C_{11}=\square$ which refers to a contradiction.

Theorem 2 A formula $\varphi$ is UNSAT if and only if there exists a resolution refutation of $\varphi$

With the definition of resolution refutation, and Theorem 2, we can also prove that a formula is valid. A formula $\varphi$ is valid, then $\lnot \varphi$ must be UNSAT.

Thus, to show $KB \models \alpha$, we only need to show $(\mbox{KB} \wedge \neg \alpha)$ is UNSAT using resolution.

Example of Resolution to Prove Valid

Given two statements, “all Greeks are mortal” and “all mortals are human”; how resolution can be used to deduce that “all Greeks are human”.

Thus the agent’s knowledge base in CNF is,

An agent want to prove that KB$\models(\neg g \vee m)$ is valid, or alternatively KB$\wedge \neg(\neg g \vee m)$ is UNSAT.

Resolve $C_1$ and $C_3$:

Resolve $C_2$ and $C_4$:

Resolve $C_5$ and $C_6$:

KB$\models(g \rightarrow m)$ is valid.

Concluding Remark

However, the order to apply resolution to derive a contradiction is still a challenging task that can take exponential time.