ARIFICIAL INTELLIGENCE- JNTUK R19- UNIT3- Logic Concepts

3. LOGIC CONCEPTS

 

PROPOSITIONAL CALCULUS (PC):

 

Propositional Calculus (PC) refers to a language of propositions in which a set of rules are used to combine simple propositions to form compound propositions with the help of certain logical operators. These logical operators are often called connectives. Examples of some connectives are not (~), and (Λ), or (V), implies (→) & equivalence (↔). A well defined formula is defined as a symbol or a string of symbols generated by the formal grammar of a formal language.

Properties of a well formed formula in PC:

 

·         The smallest unit (or an atom) is considered to be a well formed formula.

·         If α is a well-formed formula, then ~α is a well-formed formula.

·         If α and β are well formed formulae, then (α Λ β), (α V β), (α → β), (α ↔ β) are also well-formed formulae.

Truth Table:

 

In PC, a truth table is used to provide operational definitions of important logical operators. The logical constants are true & false which are represented by T & F. Let us assume A, B, C, … are propositioned symbols.

 

A	B	~A	A Λ B	A V B	A→B	A↔B
T	T	F	T	T	T	T
T	F	F	F	T	F	F
F	T	T	F	T	T	F
F	F	T	F	F	T	T

 

Example: Compute the truth value of α: (AVB) Λ(~B→A) using truth table approach.

 

Solution: Using the Truth Table approach, compute truth values of (AVB) and (~B→A) and then compute for the final expression (AVB) Λ(~B→A).

 

 

A	B	A V B	~B	~B →A	α
T	T	T	F	T	T
T	F	T	T	T	T
F	T	T	F	T	T
F	F	F	T	F	F

 

Equivalence Laws:

 

Equivalence relations (or laws) are used to reduce or simplify a given well-formed formula or to derive a new formula from the existing formula. Some of the important equivalence laws are:

 

 

 

Name of Relation	Equivalence Relations
Commutative Law	A V B ≅ B V A A Λ B ≅ B Λ A
Associative Law	A V (B V C) ≅ (A V B) V C
	A Λ ( B Λ C) ≅ (A Λ B) Λ C
Double Negation	~ (~ A) ≅ A
Distributive Laws	A V ( B Λ C) ≅ (A V B) Λ (A V C) A Λ ( B V C) ≅ (A Λ B) V (A Λ C)
De Morgan’s Law	~ (A V B) ≅ ~ A  Λ ~ B ~ (A Λ B) ≅ ~ A  V ~ B
Absorption Laws	A V (A Λ B) ≅ A A Λ (A V B) ≅ A A V (~A Λ B) ≅ A V B A Λ (~A V B) ≅ A Λ B
Idempotence	A V A ≅ A A Λ A ≅ A
Excluded Middle Law	A V ~ A ≅ T (True)
Contradiction Law	A Λ ~ A ≅ F (False)
Commonly used equivalence relations	A V F ≅ A A V T ≅ T A Λ T ≅ A A Λ F ≅ F A → B ≅ ~A V B A ↔ B ≅ (A → B) Λ (B → A) ≅ (A Λ B) V (~A Λ ~B)

 

 

Let us verify the absorption law A V (A Λ B) ≅ A using the Truth Table approach

 

A	B	A Λ B	A V (A Λ B)
T	T	T	T
T	F	F	T
F	T	F	F
F	F	F	F

 

PROPOSITIONAL LOGIC (PL):

 

Propositional Logic (or) prop Logic deals with the validity, satisfiability (also called consistency) and unsatisfiability (inconsistency) of a formula and the derivation of a new formula using equivalence laws. Each row of a truth table for a given formula α is called its interpretation under which the value of a formula may be true or false.

 

●  A formula α is said to be a tautology if and only if the value of α is true for all its interpretations.

 

Now, the validity, satisfiability & unsatisfiability of a formula may be determined on the basis of the following conditions:

·         A formula α is said to be valid if and only if it is a tautology.

·         A formula α is said to be satisfiable if there exists at least one interpretation for which α is true.

·         A formula α is said to be unsatisfiable if the value of α is false under all interpretations.

 

Example: Show that the following is a valid argument: “If it is humid then it will rain and since it is humid today it will rain”

Solution: Let us symbolize each part of the English sentence by propositional atoms as follows:

A: It is humid B: It will rain

Now, the formula (α) corresponding to the given sentence: “If it is humid then it will rain and since it is humid today it will rain” may be written as

α: [(A→B) Λ A] →B

 

The truth table for α: [(A→B) Λ A] →B is as follows

 

 

A	B	A → B = X	X Λ A = Y	Y→ B
T	T	T	T	T
T	F	F	F	T
F	T	T	F	T
F	F	T	F	T

 

Truth table approach is a simple & straight forward method & is extremely useful at presenting an overview of all the truth values in a given situation. Although it is an easy method for evaluating consistency, in consistency (or) validity of a formula, the limitation of this method lies in the fact that the size of the truth table grows exponentially. If a formula contains n atoms, then the truth table will contain 2n entries.

For example, if we have to show that a formula α: (A ΛB ΛC ΛD) → (BVE) is valid using the truth table approach, then we need to construct the table containing 32 rows & complete the truth values.

There are other methods which can help in proving the validity of the formula directly. Some other methods that are concerned with proofs & deductions are

·         Natural Deductive System

·         Axiomatic System

·         Semantic Tableaux Method

·         Resolution Refutation Method

 

NATURAL DEDUCTION SYSTEM (NDS):

 

Natural Deduction System (NDS) is thus called because of the fact that it mimics the pattern of natural reasoning. The system is based on as set of deductive inference rules. It has about 10 deductive inference rules. They are as follows

 

Example 1: Prove that A Λ (B V C) is deduced from A Λ B.

Solution: The theorem in NDS can be written as from A Λ B infer A Λ (B V C) in NDS. We can prove the theorem as follows

 

Example 2: Prove the theorem infer [(A→B) Λ (B→C)] → (A→C)

Solution: The theorem infer [(A→B) Λ (B→C)] → (A→C) is reduced to the theorem from (A→B), (B→C) infer (A→C) using deduction theorem. Further to prove ‘A→C’ we will have to prove a sub theorem from A infer C. The proof of the theorem is as follows

 

 

AXIOMATIC SYSTEM:

The Axiomatic System is based on a set of 3 axioms & 1 rule called Modus Ponen (MP). Although it is minimal in structure, it is as powerful as truth table & NDS. In this system, only 2 logical operators not (~) & implies (→) are allowed to form a formula. It should be noted that other logical operators such as and (Λ), or (V) & equivalence (↔) can be easily expressed in terms of not (~) & implies (→) using equivalence laws. For example,

·         A Λ B ≅ ~ (~A V ~B) ≅ ~ (A→ ~ B)

·         A V B ≅ ~ A → B

·         A ↔ B ≅ (A → B) Λ (B → A) ≅ ~ [(A → B) → ~ (B → A)] In axiomatic system, α, β & γ are well-formed formulae.

Axiom 1: α → (β → α)

Axiom 2: (α →(β→γ)) →((α → β) → (α → γ)) Axiom 3: (~ α → ~ β) → ( β → α)

Modus Ponen (MP) Rule: Hypotheses: α → β and α Consequent: β

Interpretation of Modus Ponen Rule: Given that α → β and α are hypotheses (assumed to be true), β is inferred (true) as a consequent.

Example 1: Establish that A → C is a deductive consequence of {A → B, B → C}, i.e.., {A→B, B→C} |- (A→ C)

 

Example 2: Prove |- ~A → (A → B) by using deduction theorem.

Solution: If we can prove {~A} |- (A → B) then using deduction theorem, we have proved |- ~A → (A → B). The proof is a shown below

 

Note: If ∑ is an empty set & α is deduced, then we can write |- α. In this case, α is deduced from axioms only & no hypotheses are used.

 

SEMANTIC TABLEAU SYSTEM IN PROPOSITIONAL LOGIC:

In both Natural Deduction & Axiomatic Systems, forward chaining approach is used for constructing proofs & derivations. In this approach we start proofs (or) derivations from a given set of hypotheses (or) axioms. In Semantic Tableau System, proofs follow backward chaining approach. In this method, a set of rules are applied systematically on a formula or a set of formulae in order to establish consistency or inconsistency.

Semantic Tableau Rules:

The Semantic Tableau Rules are given below where α & β are two formulae

 

 

Rule 1: A tableau for a formula (α Λ β) is constructed by adding both α and β to the same path (branch).

α Λ β is true if both α and β are true

 

 

Rule 2: A tableau for a formula ~ (α Λ β) is constructed by adding two new paths, one containing ~ α and other containing ~ β.

~ (α Λ β) is true if either ~ α or ~ β is true

Rule 3: A tableau for a formula (α V β) is constructed by adding two new paths, one containing α and other containing β.

α V β is true if either α or β is true

Rule 4: A tableau for a formula ~ (α V β) is constructed by adding both ~ α and ~ β to the same path.

~ (α V β) is true if both ~α and ~β are true

Rule 5: A tableau for ~ ( ~ α ) is constructed by adding α on the same path.

~ ( ~ α ) is true then α is true

Rule 6: A tableau for a formula α → β is constructed by adding two new paths: one containing ~ α and the other containing β.

α → β is true then ~ α V β is true

Rule 7: A tableau for a formula ~ ( α → β) is constructed by adding both α & ~ β to the same path.

~ ( α → β) is true then  α Λ ~β is true

Rule 8: A tableau for a formula α ↔ β is constructed by adding two new paths: one containing α Λ β and other

~α Λ ~β which are furthur expanded.

α ↔ β is true then (α Λ β) V (~α Λ ~β) is true

Rule 9: A tableau for a formula ~ ( α ↔ β) is constructed by adding two new paths: one containing α Λ ~β and the other ~α Λ β which are furthur expanded.

~ (α ↔ β) is true then (α Λ ~β) V (~α Λ β) is true

 

Example 1: Construct a Semantic Tableau for a formula (A Λ ~B) Λ (~B → C)

 

PREDICATE LOGIC:

Logic: Logic is concerned with the truth of statements about the world. Generally each statement is either True or False. Logic includes

·         Syntax

·         Semantics

·         Inference Procedure

Syntax: Specifies the symbols in the language about how they can be combined to form sentences. The facts about the world are represented as sentences in logic.

Semantic: Specifies how to assign a truth value to a sentence based on its meaning in the world. It specifies what facts a sentence refers to. A fact is a claim about the world, and it may be True or False.

Inference Procedure: Specifies methods for computing new sentences from an existing ones.

 

 

Predicate Logic: It is the study of individuals and their properties. Conside the following set of sentences:

1.    Marcus was a man.

2.    Marcus was a Pompeian.

3.    All Pompeians were Romans

4.    Caesar was a ruler

5.    All Romans were either loyal to Caesar or hated him.

6.    Everyone is loyal to someone.

7.    People only try to assassinate rulers they are not loyal to

8.    Marcus tried to assassinate Caesar.

The facts described by these sentences can be represented as a set of WFF’s (Well Formed Formula) in Predicate Logic as follows:

1.        Marcus was a man. man (Marcus)

2.        Marcus was a Pompeian.

Pompeian (Marcus)

3.        All Pompeians were Romans.

"x: Pompeian(x) → Roman(x)

4.        Caesar was a ruler. ruler (Caesar)

5.        All Romans were either loyal to Caesar or hated him.

"x: Roman(x)→loyal to (x, Caesar) V hate(x, Caesar)

6.        Everyone is loyal to someone.

"x: $y: loyal to(x, y)

7.        People only try to assassinate rulers they are not loyal to

"x: "y: person(x) ^ ruler(y) ^ try assassinate(x, y) → ¬ loyal to(x, y)

8.        Marcus tried to assassinate Caesar. tryassassinate(Marcus, Caesar)

 

Now suppose we want to use these statements to answer the question

Was Marcus loyal to Caesar?

It seems that using 7 and 8, we should be able to prove that Marcus was not loyal to Caesar. Now let’s try to produce a formal proof, reasoning backward from the desired goal:

¬ loyal to (Marcus, Caesar)

The attempt fails, however, since there is no way to satisfy the goal person(Marcus) with the statements available. We know that Marcus was a man; we do not have any way to conclude from that Marcus was a person. We need to add the representation of another fact to our system, namely:

 

9.    All men are people.                                        "x : man(x) → person(x)

Fig: An Attempt to Prove ¬ loyalto (Marcus, Caesar)

 

Now we can satisfy the last goal and produce a proof that Marcus was not loyal to Caesar. From this example, we see that three important issues must be addressed in the process of converting English sentences into logical statements and then using those statements to deduce new ones.

·         Many English sentences are ambiguous. (Ex: 5, 6, and 7 above). Choosing the correct interpretation may be difficult.

·         There is often a choice of how to represent the knowledge (1 and 7). Simple representations are desirable, but they may preclude certain kinds of reasoning.

·         Even in very simple situations, a set of sentences is unlikely to contain all the information necessary to reason about the topic at hand.

 

Representing Instance And Isa Relationships:

The below figure shows the five sentences of the last section represented in logic in three different ways. The first part of the figure contains the representations we have already discussed. In these representations, class membership is represented with unary predicates (such as Roman), each of which corresponds to a class. Asserting that p(x) is true is equivalent to asserting that x is an instance (or element) of P. The second part of figure contains representations that use the instance predicate explicitly.

The predicate instance is a binary one, whose first argument is an object and whose second argument is a class to which the object belongs. But these representations do not use an explicit isa predicate. Instead, subclass relationships, such as that between Pompeians and Romans, are described as shown in sentence 3.The implication rule there states that if an object is an instance of subclass Pompeian then it is an instance of superclass Roman. This rule is equivalent to subclass-superclass relationship. The third part contains representations that use both instance and isa predicates explicitly. The additional axiom describes how an instance relation and an isa relation can be combined to derive a new instance relation.

Statements as well-formed formulas (WFF’s):

1.    man (Marcus)

2.    Pompeian (Marcus)

3.    "x: Pompeian (x) → Roman(x)

4.    ruler (Caesar)

5.    "x: Roman (x) → loyal to (x, Caesar) V hate (x, Caesar) Statement representation using INSTANCE predicate:

1.    instance (Marcus, man)

2.    instance (Marcus, Pompeian)

3.    "x: instance (x, Pompeian) → instance (x, Roman)

4.    instance (Caesar, ruler)

5.    "x: instance (x, Roman) → loyalto (x, Caesar) V hate (x, Caesar) Statements using ISA predicate:

1.    instance (Marcus, man)

2.    instance (Marcus, Pompeian)

3.    isa (Pompeian, Roman)

4.    instance (Caesar, ruler)

5.    "x: instance (x, Roman) → loyalto (x, Caesar) V hate (x, Caesar)

6.      "x: "y: "z: instance (x, y) ^ isa (y, z) → instance (x, z)

 

 

 

Computable Functions And Predicates:

In some cases we need to exempt some cases. For example that Paulus was a roman and he never hates Caesar. So in representing the statement that all roman was hated Caesar, only Paulus need to be exempted. And hence the statement will be as follows:

"x: Roman (x) ^ ¬ equalto(x, Paulus) → loyalto(x, Caesar) V hate(x, Caesar)

These types of exceptions are very easy to represent in case of smaller number of statements. Suppose we want to express simple facts, such as the following greater-than and less-than relationships:

gt (1, 0)        lt (0, 1)

gt (2, 1)        lt (1, 2)

gt (3, 2)        lt (2, 3)    and so on.

 

If there is very large number of predicates like the above statements we can easily represent them and more over we can also simplify them if we have additional knowledge about them. That is we can infer new statements in smaller number by inferring new statements from the old.

 

1.        Marcus was a man.

Man (Marcus)

2.        Marcus was a Pompeian.

Pompeian (Marcus)

3.        Marcus was born in 40 A.D. born (Marcus, 40)

4.          All means are mortal.

"x: man(x)→ mortal(x)

5.      All Pompeian’s died when the volcano erupted in 79 A.D. Erupted (volcano, 79) ^ "x: [Pompeian (x) → died(x, 79)]

6.          No mortal lives longer than 150yers.

"x: "t1: "t2: mortal (x) ^ born (x, t1) ^ gt (t2-t1, 150) → dead (x, t2)

7.    It is now 1991 A.D. now= 1991

Now we want to answer the question is “Is Marcus alive?” For example, our statements talk about dying, but they say nothing that relates to being alive, which is what the question is asking. So we add the following facts:

8.    Alive means not dead.

"x : "t: [alive (x, t) → ¬dead (x, t)] ^ [¬dead (x, t) → alive (x, t) ]

This is an example of the fact that rarely do two expressions have truly identical meanings in all circumstances.

9.        If someone dies, then he is dead at all later times.

"x: "t1: "t2: died (x, t1) ^ gt (t2, t1) → dead (x, t2)

This representation says that one is dead in all years after the one in which one died. Now let’s attempt to answer the question “Is Marcus alive?” by proving:

 

¬alive (Marcus, now)

 

Fig: Two ways of Proving that Marcus Is Dead

 

 

RESOLUTION:

 

Resolution is a procedure used in proving that arguments which are expressible in predicate logic are correct. Resolution is so far only defined for Propositional Logic. The resolution process can also be applied to predicate logic also. Resolution produces proofs by refutation. In other words, to prove the validity of a statement, resolution attempts to show that the negation of the statement produces a contradiction with the known statements (i.e., the statement is unsatisfiable).

The Basis of Resolution:

 

The resolution procedure is an iterative process; at each step, two clauses called the parent clauses containing the same literal, are compared (resolved), yielding a new clause called the resolvent, that has been inferred from them. The literal must occur in positive form in one clause and in negative form in the other. The resolvent is obtained by combining all of the literals of the parent clauses except the ones that cancel. If the clause that is produced is an empty clause, then a contradiction has been found.

 

Given:                         winter V summer

Ø winter V cold

We can conclude: summer v cold

In predicate logic, the situation is more complicated since we must consider all possible ways of substituting values for the variables. The theoretical basis of the resolution procedure in predicate logic is Herbrand’s Theorem, which tells us the following.

·         To show that a set of clauses S is unsatisfiable, it is necessary to consider only interpretations over a particular set, called the Herbrand universe of S.

·         A set of clauses S is unsatisfiable if and only if finite subset of ground instances of S is unsatisfiable.

 

The second part of the theorem is important if there is to exist any computational procedure for proving unsatisfiability, since in a finite amount of time no procedure will be able to examine an infinite set. The first part suggests that one way to go about finding a contradiction is to try systematically the possible substitutions and see if each produces a contradiction.

 

So we observed here that to prove the statements using predicate logic the statements and well-formed formulas must be converted into clause form and the process will be as follows:

 

Conversion to Clause Form:

 

One method we shall examine is called resolution of requires that all statements to be converted into a normalized clause form .we define a clause as the disjunction of a number of literals. A ground clause is one in which no variables occur in the expression. A horn clause is a clause with at most one positive literal.

To transform a sentence into clause form requires the following steps:

 

1.  Eliminate ®.

2.  Reduce the scope of each Ø to a single term.

3.  Standardize variables so that each quantifier binds a unique variable.

4.  Move all quantifiers to the left without changing their relative order.

5.  Eliminate $ (Skolemization).

6.  Drop ".

7.  Convert the formula into a conjunction of disjuncts.

8.  Create a separate clause corresponding to each conjunct.

9.  Standardize apart the variables in the set of obtained clauses.

 

We describe the process of eliminating the existential quantifiers through a substitution process. This process requires that all such variables are replaced by something called Skolem functions. Sometimes ones with no arguments are called Skolem constants.

Example in Predicate logic: Suppose we know that “all Romans who know Marcus either hate Caesar or think that any one who hates any one is crazy”. We could represent that in the following wff:

"x: [Roman (x)Ùknow(x,marcus)] ® [hate(x,Caesar) Ú ("y: $z:hate(y,z) ®thinkcrazy(x,y))]

1.        Eliminate implies symbol using the fact that a ® b = ØaÚb.

"x:Ø[Roman(x)Ùknow(x,marcus)]Ú[hate(x,Caesar)Ú("y: Ø( $z:hate(y,z) Ú thinkcrazy(x,y))]

2.        Reduce the scope of each Ø to a single term.

"x: [ØRoman(x)ÚØknow(x,marcus)]Ú[hate(x,Caesar)Ú("y:"z:Øhate(y,z)Ú thinkcrazy(x,y))] [Ø (Ø p) = p].[Ø(a Ùb) = ØaÚ Ø b]. [Ø$x: p(x) = "x: Ø p(x)]. [Ø"x: p(x) = $x: Ø p(x)].

3.        Standardize variables so that each quantifier binds a unique variable. Since variables are just dummy names, this process cannot affect the truth value of the wff.

"x:P(x) Ú "x:Q(x) would be converted into "x:P(x) Ú "y:Q(y)

4.        Move all quantifiers to the left of the formula with out changing their relative order.

"x:"y:"z:[ØRoman(x)ÚØknow(x,marcus)]Ú[hate(x,Caesar)Ú Øhate(y,z) Ú thinkcrazy(x,y))]

5.        Eliminate existential quantifiers.

In our example, there are no existential quantifiers at step 4. There is no need to eliminate those quantifiers. If those quantifiers occur then use Skolem functions to eliminate those quantifiers. For ex:

$y: President (y) can be transformed into the formula President(S1)

"x : $y: father-of(y, x) would be transformed into "x : father-of (S2(x), x)

6.        Drop the prefix. From (4).

[Ø Roman (x) ÚØknow(x, Marcus)] Ú [hate(x, Caesar) Ú (Øhate(y, z) Ú thinkcrazy(x, y))]

7.        Convert the matrix into a conjunction of disjuncts. In our problem that are no (ands) disjuncts. So use associative property. (aÚb) Úc = aÚ(b Úc).

Ø Roman (x) ÚØknow(x, Marcus) Ú hate(x, Caesar) Ú Øhate(y, z) Ú thinkcrazy(x, y).

Ex: [winter V (summer ^ wearingsandals)] V [wearing boots V (summer ^ wearingsandals)] (winter V summer) ^

(winter V wearingsandals) ^ (wearing boots V summer) ^ (wearing boots V wearingsandals)

8.        Create a separate clause corresponding to each conjunct.

(winter V summer), (winter V wearingsandals), (wearing boots V summer), (wearing boots V wearingsandals)

 

Resolution in Propositional Logic:

 

We first present the resolution procedure for propositional logic. We then expand it to include predicate logic. In propositional logic, the procedure for producing a proof by resolution of proposition P with respect to a set of axioms F is the following.

Algorithm: Resolution Propositional

 

1.        Convert all the propositions of F to clause form.

2.        Negate P and convert the result to clause form. Add it to the set of clauses obtained in 1.

3.    Repeat until either a contradiction is found or no progress can be made:

a)    Select two clauses. Call these the parent clauses.

b)    Resolve them together. The resulting clause, called the resolvent, will be the disjunction of all of the literals of both of the parent clauses with the following exception: if there are any pairs of literals L and ØL such that one of the parent clauses contains L and other contains ØL, then select one such pair and eliminate both L and ØL from the resolvent.

c)    If the resolvent is the empty clause, then a contradiction has been found. If it is not, then add it to the set of clauses available to the procedure.

A Few Facts in Propositional Logic:

 

 

Given Axioms	Clause Form
P	P	(1)
(P L Q) ® R	ØP V ØQ V R	(2)
(S V T) ® Q	ØS V Q	(3)
	ØT V Q	(4)
T	T	(5)

 

Fig: Resolution in Prepositional Logic

 

The Unification Algorithm:

 

In propositional logic, easily determine two literals and its contradictions. Simply look for L and ØL In predicate logic, this matching process is more complicated since the arguments of the predicates must be considered. For ex: man (John) and Øman (John) is a contradiction. While man (John) and Øman (John) is not. Thus in order to determine contradictions, we need a matching procedure that compares two literals and discovers whether there exists a set of substitutions that makes them identical. The recursive procedure that will do the above called the unification algorithm.

The basic idea of unification is very simple. To attempt to unify two literals, we first check,

1.        If their initial predicate symbols are the same. If so, we can proceed, else we can’t unify them. Ex. try assassinate (Marcus, Caesar). hate (Marcus, Caesar).

2.        If the predicate symbols match, we must check the arguments, one pair at a time. If the first matches, we can continue with the second, and so on. To test each argument pair we can simply call the unification procedure recursively. The matching rules are

·         Different constants or predicates cannot match; identical ones can.

·         A variable can match another variable, any constant, or a predicate expression.

With the restriction that the predicate expression must not contain any instances of the variables being matched. For example, suppose we want to unify the expressions

P (x, x) and P (y, z)

The two instances of P match fine. Next we compare x and y, and decides that if we substitute y for x, they could match. We will write that substitute y for x → y/x.

The next match x and z, we produce the substitution z for x. → z/x. But we cannot substitute both y and z for x, we have not produced a consistent substitution. To avoid this we’ll make the substitution y/x through out the literals.

P (y, y) and P (y, z) (substitution of y/x)

Now, we can attempt to unify arguments y and z which succeeds the substitution z/y Algorithm: Unify (L1, L2)

 

1.    If L1 and L2 are both variables or constants, then:

a)  If L1 and L2 are identical, then return NIL.

b)  Else if L1 is a variable, then if L1 occurs in L2 then return {FAIL}, else return(L2/L1).

c)  Else if L2 is a variable, then if L2 occurs in L1 then return {FAIL}, else return(L1/L2).

d)  Else return {FAIL}.

2.    If the initial predicate symbols in L1 and L2 are not identical, then return {FAIL}.

 

3.    If L1 and L2 have a different number of arguments, then return {FAIL}.

4.    Set SUBST to NIL.

5.    For i ß 1 to number of arguments

a)  Call Unify with the ith argument of L1 and ith argument of L2, putting result in S.

b)  If S contains FAIL then return {FAIL}.

c)  If S is not equal to NIL then:

i.   Apply S to the remainder of both L1 and L2.

ii.    SUBST:= APPEND (S, SUBST).

6.    Return SUBST.

 

 

Resolution in Predicate Logic:

 

Algorithm: Resolution

1.    Convert all the statements of F to clause form.

2.    Negate P and convert the result to clause form. Add it to the set of clauses obtained in 1.

3.    Repeat until either a contradiction is found or no progress can be made, or a predetermined amount of effort has been expended.

a)        Select two clauses. Call these the parent clauses.

b)       Resolve them together. The resolve will be the disjunction of all of the literals of both parent clauses with appropriate substitutions performed and with the following exception: if there is one pair of literals T1 and ØT2 such that one of the parent clauses contains T1 and other contains T2 and if T1 and T2 are unifiable, then neither T1 nor T2 complementary literals. Use the substitution produced by the unification to create the resolvent. If there is more than one pair of complementary literals, only one pair should be omitted from the resolvent.

c)        If the resolvent is the empty clause, then a contradiction has been found. If it is not, then add it to the set of clauses available to the procedure.

 

 

 

 

 

 

 

 

 

 

Fig: A Resolution Proof

 

9.    persecute (x, y) → hate (y, x)

10.     hate (x, y) → persecute (y, x) Converting to clause form we get

9.    Øpersecute (x5, y2) V hate (y2, x5)

10.     Øhate (x6, y3) V persecute (y3, x6)

Now to detect that there is no contradiction we must discover that the only resolvents that can be generated before. In other words, although we can generate resolvents, we can generate no new ones.

 

Fig: An Unsuccessful Attempt at Resolution

 

 

Fig: Using Resolution with Equality and Reduce