Resolution in AI
The resolution technique is an inference rule that has distinct applications in propositional and first-order predicate logic. This technique is essentially used to demonstrate a sentence's satisfiability.
In 1965, a mathematician named John Alan Robinson created it. When multiple statements are provided and a conclusion needs to be proven, resolution is employed.
A fundamental idea in proofs by resolutions is unification. Conjunctive normal form or clausal form can be effectively operated on by a single inference rule called resolution.
Clause: A clause is the disjunction of literals. Another name for it is a unit clause.
Conjunctive Normal Form: A sentence is considered to be in conjunctive normal form when it is expressed as a conjunction of clauses.
Resolution Inference Rule in AI
If two clauses have complimentary literals—literals that are presumed to be standardized apart so they share no variables—resolution can resolve them.
Q or R is true if both P or Q and not P or R are true.
P: It's pouring with rain.
Q: The streets are wet.
R: The roads are slick.
Notation:
((𝑃 ∨𝑄 ) ∧ (∼ 𝑃 ∨𝑅 ) ) ⇒ (𝑄∨𝑅) ((P∨Q)∧(∖P∨R))→ (Q∧R)
Example of Resolution Inference Rule
Streets are wet or roads are slippery (Q∨R) because it is raining or the streets are wet (P∨Q) and it is not raining or the roads are slippery (~P∨R).
Unification in AI
Finding a replacement allows two distinct logical atomic expressions to become identical, a process known as unification. Substitution is the procedure that leads to unification. It uses substitution to make two literals that are entered into it identical.
It is the process of giving variables values that enable several phrases or concepts to match or unify, so making them identical.
In knowledge representation, logic programming, and natural language processing, unification is essential because it allows artificial intelligence (AI) systems to reason, infer, and deal with uncertainty by bringing different pieces of information together.
Conditions for Unification
- Atoms or expressions with distinct predicate symbols cannot be united; the predicate symbol must always be the same.
- There must be an equal number of arguments in each formulations.
- If two comparable variables appear in the same expression, unified expression will fail.
Example of Unification in AI
Expression 1: p ( x, f(y) )
Expression 2: p (a, f(g (z) )
If a is substituted for x and g (z) for y, then expressions 1 and 2 are the same.
Set of substitutions: [ a/x, g(z)/y ]
Algorithm of Unification in AI
The Unification Algorithm (A1, A2)
Step 1:
(a) If A1 or A2 is variable, then A1 and A2 are identical, then Return = Null.
(b) Return = fail if A1 appears in A2.
(c) Look for A2 in A1. Return = A2/A1
(d) else If A2 appears in A1, then fail; otherwise, return (A1,A2).
Step 2: If the predicate is not the same.
Step 3: If different arguments.
Step 4: Else, Subset = NULL.
Step 5: Repeat LOOP.
Step 6: Return Subset.
