Inference in First-Order Logic in Artificial intelligence
In this page we will learn about Inference in First-Order Logic in Artificial intelligence, Substitution, Equality, FOL inference rules for quantifier, Universal Generalization, Universal Instantiation, Existential Instantiation, Existential introduction, Generalized Modus Ponens Rule.
Inference in First-Order Logic
In First-Order Logic, inference is used to derive new facts or sentences from existing ones. Before we get into the FOL inference rule, it's important to understand some basic FOL terminology.
Substitution:
Substitution is a basic procedure that is applied to terms and formulations. It can be found in all first-order logic inference systems. When there are quantifiers in FOL, the substitution becomes more complicated. When we write F[a/x], we are referring to the substitution of a constant "a" for the variable "x."
[ Note: first-order logic can convey facts about some or all of the universe's objects. ]
Equality:
In First-Order Logic, atomic sentences are formed not only via the use of predicate and words, but also through the application of equality. We can do this by using equality symbols, which indicate that the two terms relate to the same thing.
Example: Brother (John) = Smith.
In the above example, the object referred by the Brother (John) is close to the object referred by Smith. The equality symbol can be used with negation to portray that two terms are not the same objects.
Example: ¬(x=y) which is equivalent to x ≠y.
FOL inference rules for quantifier:
First-order logic has inference rules similar to propositional logic, therefore here are some basic inference rules in FOL:
- Universal Generalization
- Universal Instantiation
- Existential Instantiation
- Existential introduction
1. Universal Generalization:
- Universal generalization is a valid inference rule that states that if premise P(c) is true for any arbitrary element c in the universe of discourse, we can arrive at the conclusion x P. (x).
- It can be represented as:
- If we want to prove that every element has a similar property, we can apply this rule.
- x must not be used as a free variable in this rule.
2. Universal Instantiation:
- A valid inference rule is universal instantiation, often known as universal elimination or UI. It can be used to add additional sentences many times.
- The new knowledge base is logically equal to the existing knowledge base.
- We can infer any phrase by replacing a ground word for the variable, according to UI
- The UI rule say that we can infer any sentence P(c) by substituting a ground term c (a constant within domain x) from ∀ x P(x) for any object in the universe of discourse.
- It can be represented as
"John likes ice-cream" => P(c)
Example: 2 Let's take a famous example,
"All kings who are greedy are Evil." So let our knowledge base contains this detail as in the form of FOL: ∀x king(x) ∧ greedy (x) → Evil (x),
We can infer any of the following statements using Universal Instantiation from this information:
- King(John) ∧ Greedy (John) → Evil (John),
- King(Richard) ∧ Greedy (Richard) → Evil (Richard),
- We can infer any phrase by replacing a ground word for the variable, according to UI
- King(Father(John)) ∧ Greedy (Father(John)) → Evil (Father(John)),
3. Existential Instantiation:
- Existential instantiation is also known as Existential Elimination, and it is a legitimate first-order logic inference rule.
- It can only be used to replace the existential sentence once.
- Although the new KB is not conceptually identical to the old KB, it will be satisfiable if the old KB was.
- This rule states that for a new constant symbol c, one can deduce P(c) from the formula given in the form of x P(x).
- The only constraint with this rule is that c must be a new word for which P(c) is true.
- It's written like this:
From the given sentence: ∃x Crown(x) ∧ OnHead(x, John),
So we can infer: Crown(K) ∧ OnHead( K, John), as long as K does not appear in the knowledge base.
- The above used K is a constant symbol, which is known as Skolem constant.
- The Existential instantiation is a special case of Skolemization process.
4. Existential introduction
- An existential generalization is a valid inference rule in first-order logic that is also known as an existential introduction.
- This rule argues that if some element c in the universe of discourse has the property P, we can infer that something in the universe has the attribute P.
- It's written like this:
- Example: Let's say that,
"Priyanka got good marks in English."
"Therefore, someone got good marks in English."
Generalized Modus Ponens Rule:
In FOL, we use a single inference rule called Generalized Modus Ponens for the inference process. It's a modified form of Modus ponens.
"P implies Q, and P is declared to be true, hence Q must be true," summarizes Generalized Modus Ponens.
Modus Ponens states that for atomic phrases pi, pi', q. Where there is a substitution θ such that SUBST (θ, pi',) = SUBST(θ, pi), it can be represented as:
Example: We will use this rule for Kings are evil, so we will find some x such that x is king, and x is greedy so we can infer that x is evil.