The Equality Predicate in Artificial Intelligence

The Equality Predicate 

• In a knowledge base the formulas consists of relational constants which have their intended meanings but they are restricted by some of the set of models of knowledge base. 
• The consistency of the results of resolution refutation is achieved by suitable constraints imposed by the knowledge base for the actual relations. 
• The frequently occurring relations should also be described by knowledge base to know their intended meaning. 
• Equality relation is. an example of commonly occurring relation. 
• It can be represented as equals (A, B) which is the prefix form. 
• The relation constant in infix form for equality is A = B. 
• By knowing the relation we cannot know whether P(A) can conclude P(B) or we cannot resolve Q(A, B) from ᆨQ(B, A) etc. 
• So additional formulas are required to be present in the knowledge to know the intended meaning of A = B. 
• The properties that can be added to knowledge base regarding equality are, 
• 1) It is reflexive 
• (∀x) equals (x, x) 
• 2) It is symmetric 
• (∀x, y) [Equals (x, y) ⊃ Equals (y, x)] 
• 3) It is transitive 
• (∀x, y, z) [Equals (x, y) በ (Equals (y, z) (y, z) ⊃ Equals (x, z)] 
• From these properties we cannot resolve P(B). from P(A) so the knowledge base must provide a list of substitutions for every predicate constant and function constant. This is an impractical requirement.
• Paramodulation: If the knowledge base contains the equality predicate, This rule is used along with resolution. This is a practical choice.
• Definition of Paramodulation: r_{1 and} r₂, are two clauses where r₁ = {λ(τ) ∪ r'₁} and r₂ ={Equals (∝, β) ∪ r'₂}. Here r'₁, r'₂ are clauses τ, ∝, β are terms λ(τ) is a literal that consists of the term τ, a binary paramodulant of r_{1 and} r₂ is inferred if τ and ∝, have a most general unifier ∝, 
• π = {λσ [(βσ)] ∨ r'₁σ  ∨ r'₂}
• The results of replacing ,an occurrence of πσ in  λσ by  βσ is denoted by λσ[(βσ)] 
• Now let us prove P(B) from P(A) and Equals(A, B) i.e., (A ,= B) 
• If resolution refutation is used we must get Nil from the clauses ᆨP(B), P(A) and (A = B). 
• By using paramodulation we can assign, 
• λ(τ) → P(A) 
• τ → A
• ∝ → A
• β → B 
• A which is in the role of τ and A which is in the role of ∝ unify without the use of substitution, then P(B) is the binary paramodulant obtained as a result of changing the occurrence of τ with β i.e., B. 
• Now by resolving P(B) with ᆨP(B) will give an empty clause i.e., Nil. 
• For example the binary paramodulant of P(g(f(x))) ∨ Q(x) and [f(g(B)) = A] ∨ R(g(c)) is P(g(A)) ∨ Q(g(B)) ∨ R(g(C))
• If the kinds of paramodulants are allowed to be beyond binary ones it can be combined with resolution refutation which is complete for the knowledge bases which contains equality predicate. 
• The power of paramodulation is not required in cases where there is no requirement for substituting equals for equals.
• Predicate evaluation can be used in such cases by replacing the predicate with T or F which is appropriate if an the truth value of equality predicate is returned by an external process. 
• The clauses which contains the literal T can be eliminated and the literal F in any clause can be eliminated In resolution refutation. 
• Example: If a process A is in p, a room R1 then it cannot be in room R2. The statements in the knowledge base of robot are as follows, 
• (∀x, y, u, v) [In(X, u) ∧ (u ≠v)] ⊃ ᆨIn(X, v) In(A, R1)
• Now we attempt to prove ᆨIn(A, R2). So we convert the formula into clause form. 
• ᆨIn(X, u) ∨ (u = v) ∨ ᆨIn(X, v)
• This process does not deal with the equality predicates till the wff contains ground terms. 
• Now by resolving the clause with the negation of wff which has to be proved gives. 
• (R2 = v) ∨ ᆨIn(A, v)
• Again by resolving with given wff i.e., A is R1 In(A, R1) gives (R2 = R1). 
•  As the rooms are different the knowledge base of robot may contain the wff ᆨ(R2 = R1). 
• If ᆨ(R2 = R1) is present (R2 =, R1) and ᆨ(R2 = R1) will yield an empty clause which completes the process of refutation. 
• This process may become complex in base of lame number of rooms like if there are N rooms it is needed there are  N(N -1)/2in equalities. 
• If the reasoning is done by involving numbers it may lead to large set of wffs such as ᆨ(5642 = 896). 
• So inorder to avoid .this. problem of having large set of wffs 'in knowledge base, a routine is provided so that it will evaluate the expressions like (∝ = β) ∀ ∝ground and β. 
• In the example for the expression (R2 = R1) it would return F so that the refutation can be completed. 
• Many of the relations like greater than, less than and functions like plus, times, divides can be evaluated directly instead of reasoning with formulas. 
• In automated reasoning systems the evaluation of expressions is a powerful, efficiency enhancing tool.