Chapter 9 - Inference in First-Order-Logic

Question 1

Themes

Answer 1

Inference for quantifiers

Reduce from FOL to Propositional logic

Construction of inference rules

Families of first order logic inference algorithms

Question 2

What is the “simplest” way of doing inference on first order logic?

Answer 2

The simplest way is probably to convert FOL to propositional logic.

Vx King(x) AND Greedy(x) => Evil(x)

This we could convert to propositional logic by listing all the individual instances of x. Richard, John, Father(John) etc

This is essentially called “Universal Instantiation”

Question 3

What is a universally quantified variable?

Answer 3

A universally quantified variable is a variable that goes through ALL objects in the domain, and is applied to a logical statement.

Question 4

What is a ground term?

Answer 4

A ground term is a term that contains no variables. It will be a constant symbol, or a function symbol. The point is that we KNOW the object we are considering.

Question 5

What is Universal Instantiation?

Answer 5

Universal instantiation is an inference rule that connects a specific object to a general/universal statement.

It is about being able to substitute the universally quantified variable with a constant symbol (object), also known as a ground term, and still get a result that is true.

Question 6

Consider the substitution {x/John}, what does this mean?

Answer 6

It means that we replace occurence of x with John.

Question 7

Elaborate on SUBST(theta, alfa)

Answer 7

SUBST(delta, alfa) is the result of applying the substitution “delta” to the sentence “alfa”.

Question 8

Formally, the inference rule of Universal instantiation can be written like this:

Vx P / SUBST({x/g}, P)

Elaborate on this

Answer 8

It says that for all x, P is true. And in these cases, we get that the applying the substitution x/g gives us some result.

g is basically a ground term corresponding to each individual value of the variable x.

P is a statement that is true for all x.

IMPORTANT:
The rule basically says that for all instances of a universally quantified variable x, we can receive a new sentence by replacing/substituting a ground term in for the variable.

Question 9

Recall what an existential statement actually is

Answer 9

Ex P

The statement says that “There exists at least one variable x in our domain, for which the statement P is correct/true”.

Question 10

Elaborate on EI:

Ev a / SUBST({v/k}, a)

Answer 10

EI says that: There exists at least one v that makes the statemetn/sentence a true, which will give us the opportunity to substitute this specific instance with a NEW constant symbol that represent this specific case. IMPORTANT: k must be a NEW symbol, so that we dont infer shit about old terms in our KB.

Due to the nature of the existential quantifier, we only need a single instance.

In logic, we call the new name a “Skolem constant”

Question 11

What is a “skolem constant”?

Answer 11

Skolem constant is what we call the new name used in EI

Question 12

What is the point of EI and UI?

Answer 12

To remove the quantifiers so that we can apply inference to the statements.

Question 13

In very broad terms, how do we convert a KB that use first order logic to a KB that is only propositional?

Answer 13

For UI, we instantiate all possible ground terms/objects we have in domain/KB.

For EI we need only one.

Then we replace atomic sentences, such as King(John), with propositional symbols like “JohnIsKing”.

Then we apply some complete inference algorithm to get a conclusion like “JohnIsEvil”, which is equivalent to Evil(John).

NOTE: If the knowledge base includes a function symbol, the set of possible ground terms become infinite. This is due to the nesting that may occur. For instance, Father(John), Father(Father(John)) etc.
There is a theorem that sort of avoids this though.

Question 14

Elaborate on how to avoid the problem of inifnite ground terms/nests while using function symbols

Answer 14

There is a theorem that says the following:

If a sentence x is entailed by the original knowledge base, then it will involve just a finite subset of the propotionalized knowledge base. Therefore, we know that if the sentence is in fact entailed by KB, it will be within a finite nesting. Therefore, we can explore depths incrementally until we find the answer.

NB VERY IMPORTANT: We cannot actually tell if a sentence is entailed or not by this method, as if the sentence is not entailed, the algorithm would ocntinue infinitely long. This resemble the halting problem.

In other words, we have algorithms that can verify entailment, but not solve it.

Question 15

Say we have the following rule in our KB:

King(x) AND Greedy(x) => Evil(x)

How can we answer the query Evil(x)?

Answer 15

We want to find x that are evil.

We want to use the rule, the implication. if we can manage to find some x that satisfy being king and being greedy, then this x will be our result.

In order for the conclusion of the implication to yield true, we need both conjuncts of the premise of the implication to yield true. To do this, we need to find some sentences in our KB that serve as substitutions for the conjuncts in the premise. The subsitution is key.

Say we already have in our KB that Greedy(John)
King(John)
Then we’d solve it immediatly. Therefor,e the substitution delta = {x/John} would achieve the aim.

Question 16

Suppose we have the following rules in our KB:

King(x) AND Greedy(x) => Evil(x)
King(John)
Vy Greedy(y). “for all y, Greedy(y)”

How do we answer the query Evil(x)?

Answer 16

We would still like to conclude that Evil(John), because we know that John is a king and John is greedy, because all people are greedy.

We need to find a substituon delta for both variables in the implication sentence and the variables in the sentences that are in the knowledge base.
If we use the substitution delta={x/John, y/John}, we get the following:

RULE = King(John) AND Greedy(John)
KB = King(John), Greedy(John)
They become identical. Thus we can infer the consequent of the conclusion.

What we have done here, is to basically find some substitution for variable x and y that make the rule true based on facts from our kb.

Question 17

Elaborate on generalized modus ponens

Answer 17

Generalized modus ponens is strictly speaking not reserved for first order logic. However, we are considering the “lifted” version, which takes substitutions into account.

For atomic sentences p_i, p_i* and q, where there is a substitution delta such that:

SUBST(delta, p_i*) = SUBST(delta, p_i) for all i, then:

(p_1, p_2, …, p_n*, (p_1 and p_2 and … and p_n => q)) / SUBST(delta, q)

What does this mean?
The atomic sentences, as we remember, are sentences without logical connectives. They are facts.
So, if we have a list of these facts, and a list of other facts that are involved in an implication rule, then we are looking for the following: We are looking for a substitution that make the conjuncts in the premise of the implication rule true by showing that the other facts we have in the KB can be substituted to the conjuncts facts by using the substitution.
If this happens to be the case, we get the result of SUBST(delta, q) which gives the sentence q when we apply substitution delta.

There are n atomic sentences (facts in KB), and one implication. The conclusion is the result of applying the substitution delta to the conclusion q.

Note that the substitution delta must apply to ALL i.

Generalized modus ponens is sound.

Question 18

What does it mean that generalized modus ponens is lifted?

Answer 18

Lifted means that it has been transferred from variable-free propositional logic to be applicable to first-order logic.

Question 19

What is unification?

Answer 19

Unification is the process of finding a substitutiuon that make different logical expressions look identical.

The UNIFY algorithm takes two sentences and returns a unifier for them (a substitution) if one exists.

UNIFY(p,q) = delta, where SUBST(delta, p) = SUBST(delta, q)

Question 20

Elaborate on how unification, and the UNIFY algorithm, should work on a query like this:

AskVars(Knows(John, x))

Answer 20

this query asks: Whom does John know? It wants a list of objects that John knows.

Answers to this query can be found by finding all sentences in the KB that unify with Knows(John, x).

for instance:
UNIFY(Knows(John, x), Knows(John, Jane)) = {x/Jane}

UNIFY(Knows(John, x), Knows(y, Bill)) = {x/Bill, y/John}

UNIFY(Knows(John, x), Knows(x, Elizabeth)) = failiure

The reason why the last one fails, is because we cannot take on the values “John” and “Elizabeth” at the same time.
The KB rule/sentence Knows(x, Elizabeth) actually means that everyone knows elizabeth, so we should be able to infer that John knows elizabeth. But the problem arise because the two sentences happen to use the same variable name.

Question 21

Elaborate on more general unifiers

Answer 21

Recall that a unifier is a substitution that make two sentences identical.

A unifier is more general if it place fewer restrictions on the values of the variables. It is relevant in the case where we have multiple possible unifiers (substitutions).

For instance, if we consider Unify(Knows(John, x), Knows(y,z)), we can get the following results:
{y/John, x/z} OR {y/John, x/John, z/John}. The first gives Knows(John, z) while the second gives Knows(John, John).

We say that the first is more general than the second because the second can be obtained from the first by adding an additional substitution {z/John}. It places fewer restrictions on the variables.

Question 22

What is standardizing apart?

Answer 22

Standardizing apart refers to renaming variables in ONE of the sentences that are being unified. This avoids name clashes.

Question 23

Recall what definite clauses are.

Answer 23

Definite clauses are disjunctions of literals of which exactly one is positive.
Therefore, definite clauses have 2 choices:

1) Be atomic, and consist of a single positive literal

2) Be like this: !a v !b v … v x
where x is the only positive literal.

Considering option #2, we can apply logical equivalences and put transform it:

(!a v !b v … v !c) v x

de Morgan:

!(a v b v … v c) v x

Reverse implicit elimination

a v b v … v c => x

Question 24

If you see an “x” (variable) in a definite clause, what does it mean?

Answer 24

Implicit universal quantifier.

For instance, Greedy(y) is interpreted as “everyone is greedy” due to the implicit universal quantifier.

Question 25

Translate this sentence into first order definite clause:

“… It is a crime for an American to sell weapons to hostile nations”

“Nono …. has some missiles”

“All of its missiles were sold to it by Colonel West”

“Missile is a weapon”

“Enemy of america is hostile”

“West, who is american…”

“the country Nono, an enemy of america…”

Answer 25

FOL definite clause can be written on the form of an implication with only positive literals.

a AND b AND c AND d … => x

American(x) AND Sell(x, y, z) AND Weapon(y) AND Hostile(z) => Criminal(x)

Ex Owns(Nono, x) AND Missile(x), this is transformed into 2 definite clauses by EI:
Owns(Nono, M_1)
Missile(M_1)

Missile(x) AND Owns(nono, x) => Sells(West, x, Nono)

Missile(x) => Weapon(x)

Enemy(x, America) => Hostile(x)

American(West)

Enemy(Nono, America)

These are all facts, except for the first one which is the statement we are itnerested in.

Question 26

How does a simple forward chaining algorithm work?

Answer 26

It will start from known facts, and trigger all rules whose premises are satisfied, adding their conclusions to the known facts.
This process repeats until the query is answered or no new facts are added.

NB: A fact is not added/new if it is just a renaming of a known fact.

The point is that we are using first-order logic with implicit universal quantifiers, and we want to find the answers to a query. If our entire KB is only definite clauses, we can use forward chaining.

Question 27

What is the strength of resolution?

Answer 27

Resolution works for every knowledge base, not just the ones with definite clauses

Question 28

Regarding resolution in first order logic, what is the first step?

Answer 28

First step is to convert to CNF. Conjunction of clauses.

This is the key because EVERY sentence of first order logic can be converted into an inferentially equivalent CNF sentence.

Question 29

What are the steps of converting FOL to CNF

Answer 29

1) Eliminate implications

2) Use de Morgan to move “!” inwards

3) Standardize variables

4) Skolemize. Skolemization is the process of removing existential quantifiers by elimination.

5) Then we drop the universal quantifier symbol, because it is become implicit with x.

6) Then we distribute OR over AND

Now we have a CNF sentence that is close to impossible to read, but is now applicable to resolution.

Question 30

Elaborate on skolemizaiton.

Whendo we use it?

Answer 30

Skolemization refers to a process of getting an expression to only include universal quantifiers.

The general rule of skolem functions is that the arguments of skolem functions are all the universally quantified variables in whose scope the existential quantifier appears.

We use skolemization when we convert a sentence to CNF. We only want universally quantified variables, becasue they carry no uncertainty.
We apply skolemization right after we have standardized the variables in the sentence, which we do right after moving the negation-signs inwards.
After skolemization, we drop the universal quantifier symbols, and then destribute over and and or.

Question 31

Elaborate on why we use “if” with implications like this:

Vx[Vy Animal(y) => Loves(x,y)] => [Ey Loves(y,x)]

“For every individual, if the indiviual loves all animals, then the individual is loved by at least someone”

Answer 31

We have to use “if” because of the nature of the conditional statement.
It is not because the statement will yield otherwise, but it is to indicate that we are using a conditional.

it is easier to understand why when looking at conditionals/implications that are not nested. Because, in this specific case, we know from our rules that the inner implication will always yield true. and since it will always yield true, the conclusion will also always be true. However, that is specific to our KB. If the condition/premise of the outer implication happened to be dependent on some random value instead, if would make more sense to use “if” when describing the outcome. This mainly to hedge against the case where the premise is false and the conclusion is true.

Question 32

What is the difficult step in transforming FOL to CNF?

Answer 32

Skolemization. Recall that skolemization is the process of removing the existential qantifiers. However, we cannot just do it without any consideration.

We replace the Existential variables with a Skolem function. This function needs to have the variables (be a function of variables) that were used by the universal quantifier INSIDE of the scope of the existential quantifier that we are removing.

The “scope” of quantifier is simply the area which it affects. The area that the quantifier applies to. Or, not area, but rather the expression it applies to.

so, if some existential quantifier applies to a sub-sentence that use 2 universally quantified variables, than these two variables must be part of the arguments of the Skolem function that we replace the existential variable with.

Question 33

Regarding resolution in first order logic, when will 2 literals complement each other?

Answer 33

The very same principle from regular resolution still applies. We need to find to expressions that are identical and complementary to each other. Therefore, we find a substitution that allows this.

In first order logic, a literal complement another literal one unifies with the negation of the other.

Example:

We have 2 clauses:
1) [Animal(F(x)) OR Loves(G(x), x)]

2) [!Loves(u,v) OR !Kills(u,v)]

We see that both use Loves. Therefore, we can get them to be idneticial by using the proper substitution.

If we use the unifier delta={u/G(x), v/x} we can produce the following clause by resolution:

[Animal(F(x) OR !Kills(u, v)]

This is called the binary resolution rule (corresponds to the unit-resolution).

The binary resolution rule by itself does not yield a complete inference procedure.

Question 34

Recall generalized modus ponens

Answer 34

Generalized modus ponens is an inference rule that work on multiple facts.

Say we have a rule in our knowledge base. This rule has form like this:
a and b and c … and x => q.

Our goal with the inference rule, is to conclude with q. If this was propositional logic, this would easily be done with something like resolution or forward checking. However, due to the presence of first order logic (objects etc), we need to be more considering.

To handle quantifiers and their variables, we are looking for a substitution (often called delta) that satisfy the quantified statements AND the rule. So, we need a substitution delta that makes the premise of the “rule” identical to the conjunction of individual facts in our knowledge base.

Formally, the generalized modus ponens rule looks like this:

p1, p2, …, p*n, (p1 AND p2 AND …AND pn => q) / subst(delta, q)

So, the result will be a sentence that no longer use quantified variables, but now use the substitution that make the conjunction of facts equal to the premise of the rule we are using.

Question 35

Explain what unification is

Answer 35

Unification is a process where we look at two first order sentences, and return a unifier. The unifier is a substitution (if one exists) that make the two sentences equal.

UNIFY(p,q) = delta
Where Subst(delta, p) == Subst(delta, q)

Make no mistake: The so-called “unifier” is the specific substitution “delta”.

Question 36

Elaborate on standardizing apart,

Answer 36

Standardizing apart is the process of renaming variables to avoid clashes. For instance, this sentence will cause chaos:
UNIFY(Knows(John, x), Knows(x, Elsa))
we cannot apply substitiuon of several values to x. THerefore, we rename the variables to avoid the problem.

Question 37

UNIFY returns a unifier (a substitution) that make two sentences look the same. What happens if we have multiple choices for substitutions?

Answer 37

Case could look like this:

UNIFY(Knows(John, x), Knows(y,z))

From this, we would return the substitution {y/John, x/z} or it could return {y/John, x/John, z/John}.

The first one is more general though. We are most interested in the most general substition.

Question 38

Consider forward chaining.What are the requirements?

Answer 38

Just like with propoisitonal logic, we need definite clauses only. Still applies to first order logic.

Question 39

Recall the two possible forms of the definite clause.

How do they appear with quantifiers?

Answer 39

The requirement is exactly one positive literal. Therefore, the clause will either be an atomic “fact” or be a shite that can be transformed into implication with premise and conclusion.

Existential quantifiers are not allowed. This is because forward-chaining is a data-driven approach that only deals with facts. We are dealing with facts, and conjunctions of facts that lead to certain conditions. There is no room for uncertainty in such a setup.
Existential quantifier would say “there exist some case where this statement is true”. This does not give us what we want, since we want to only deal with the proven facts.

King(John)

King(x) AND Greedy(x) => Evil(x)

The KEY PART is that we never write the explicit symbol for the universal quantifier. We let it be implicit as the existential is not allowed.

Question 40

Consider the definite clause “King(x)”.
What does this say?

Answer 40

It says that all objects are kings.

Question 41

Elaborate on how the simple forward chaining algorithm works

Answer 41

Sort of like the one in chapter 7.

We start with the known facts, and triggers a conclusion if a premise is satisfied fully.
This continue until the query is answered, or if no new facts are being added.

Recall that “renaming” variables is not consideirng new facts. Still the same fact.

The algorithm has parameters KB and x. x is a sentence (atomic sentence). x is thus a query of a fact.type thing.

while true{
new = {} //The set of new sentences inferred on each iteration

for each rule in KB{
(p1andp2and…andpn=>q) = standarize-variable(rule)

for each delta such that subst(delta, p1ANDp2ANd…ANDpn) = Subst(delta, p1andp2and…andpn) for some (p1, p2,…) in KB {
q = Subst(delta, q)

if q* does not unify wiht some sentence in KB or new, then
}
}
}
***
fuck this algo.

this is what it does:

On each iteration, it adds to KB all the atomic sentences that can be inferred in one step from the implication sentences and atomic sentences already in the KB

Question 42

What is the “conjunct ordering problem”?

Answer 42

Consider rule on the form:

Missile(x) AND Owns(Nono, x) => Sells(west, x, nono)

we could loop through all objects owned by Nono, and then see if it is a missile. However, if KB contains many objects owned by Nono, but very few missiles, it would be faster to loop through all missiles and check if they are owned by Nono.

Thus, the conjunct ordering problem is an efficiency problem.

Question 43

Consider the process of converting a first order statement on CNF. What differs from this and with propositional logic?

Answer 43

in first order logic, we need to remove all existential quantifiers. We’re ok with universal

Question 44

Consider first order resolution. How this this resolution rule differ from the rule we use in propositional logic?

Answer 44

It is basically the same thing. But in first order logic, we have objects, relations and funcitons, and them lot use quantified variables (universally). Since we have universally quantified variables in the expression, we have to do some work before we can resolve a pair. The pair must be identical (but complementary to each other). Therefore, we need to find a substitution that allows us to do this.

In propositional logic, we can remove a pair of literals if they are complements of eachother.

In first order logic, we obviously want the negation to stand, since we are looking for a pair to remove. However, we can only resolve the pair if they are identical, but complements. Therefore, we need to find a substitution that make them identical, but complements

Question 45

Elaborate deeply on the resolution rule in first order logic

Answer 45

IN first order logic, two literals resolve if one literal unify with the negation of the other. Meaning, one literal will resolve with another literal, if the first one and the negation of the second one CAN become identical with some substitution theta. Therefore, if such delta (substitution) exists, we can resolve.