In this article we will discuss about:- 1. Resolution in Propositional Logic 2. Soundness and Completeness of Resolution in Propositional Logic 3. Limitations.
Resolution in Propositional Logic:
Resolution is a rule of inference leading to a refutation theorem—theorem proving technique for statements in propositional logic and first- order logic. In other words, iteratively applying resolution rule in a suitable way allows for telling whether, a propositional formula (WFF) is satisfiable. Resolution was introduced by Alam Robinson in 1965.
The following steps should be carried out in sequences to employ it for theorem proving in propositional using resolution:
Resolution Algorithm:
ADVERTISEMENTS:
Given:
A set of clauses, called axioms and a goal.
Aim:
To test whether the goal is derivable from the axioms.
ADVERTISEMENTS:
Begin:
1. Construct a set S of axioms plus the negated goal.
2. Represent each element of S into conjunctive normal form (CNF) by the following steps:
(a) Replace ‘if-then’ operator by NEGATION and OR operation by theorem using 10.
ADVERTISEMENTS:
(b) Bring each modified clause into the following form and then drop AND operators connected between each square bracket. The clauses thus obtained are in conjunctive normal from (CNF). It may be noted that pij may be in negated or non-negated form.
3. Repeat:
(a) Select any two clauses from S, such that one clause contains a negated literal and the other clause contains its corresponding positive (non-negated) literal.
ADVERTISEMENTS:
(b) Resolve these two clauses and call the resulting clause the resolvent. Remove the parent clauses from S.
Until a null clause is obtained or no further progress can be made.
4. If a null clause is obtained, then report: “goal is proved”
Example 1:
ADVERTISEMENTS:
We are given the axioms given in the first column of table 6.3, and we want to prove R. First we convert the axioms to clause form, as shown in the second column of the table. Then we negate R, producing ¬ R which is already in clause form it is added into the given clauses (data base).
Then we look for pairs of clauses to resolve together. Although many pair of clauses can be resolved, only those pairs which contain complementary literals will produce a resolvent which is likely to lead to the goal shown by empty clause (shown as a box). We begin by resolving R with the clause ¬ R since that is one of the clauses which must be involved in the contradiction we are trying to find. The sequence of contradiction resolvents of the example in table 6.3., is shown in Fig. 6.4.
The procedure adopted in the above example can be explained as follows:
Resolution process starts with a set of clauses all assumed to be true. The clause 2 becomes true when either ¬ P or ¬ Q or R is true. Since ¬ R is assumed to be true, clause 2 remains true for either ¬ P or ¬ Q. This is the first resolvent clause. Now the proposition 1 says that P is true meaning thereby that ¬ P cannot be true. This leaves only one possibility ¬ Q for clause 2 to be true. This is shown by second resolvent. Proposition 4 can be true if either ¬ T or Q is true.
But ¬ Q must be true, so for proposition 4 to be true the only way for clause 4 to be true is for ¬ T to be true, shown as third resolvent. But clause 5 says that T is true. This produces contradiction (an empty box, the last resolvent). Thus with the given knowledge base all the clauses cannot be true in a simple interpretation.
A contradiction occurs when a clause becomes so restricted that there is no way it can be true. This is indicated by the generation of the empty clause. If a contradiction exists then eventually it will be found, when no contradiction exists it is possible that the procedure will never terminate, although there are other ways of detecting that no contradiction exists.
How, then can it lead to a complete inference procedure for all of propositional logic? The answer is that every sentence of propositional logic is logically equivalent to a conjunction of disjunctions of literals. A sentence expressed as a conjunction of disjunctions of literals is said to be in a Conjunctive Normal Form (CNF). Example of CNF is (P ∨ ¬ Q) ∧ (Q ∨ ¬ R ∨ ¬ S) A sentence can also be written in Disjunctive normal form (DNF), for example (P ∧ Q) ∨ (P∧¬ R) ∨ (P ∨ ¬ S) ∨ (¬ Q ∧ ¬ R) ∨ (¬ Q ∧ ¬ S).
DNF and CNF exist for all knowledge bases, and are called standarised forms of sentences. DNF form is rarely used in resolution method of problem solving.
Horn Clause is a clause which at the most one positive literal, for example, (PV ˥Q) ∧ (Q ∨ ˥R ∨ ˥S).
Definite clause is a horn clause with exactly one positive literal. If some facts are true then one fact is implied. Not all the knowledge bases can be written in Horn form.
The resolvent procedure applies only to disjunctions of literals, so knowledge bases and relevant queries should consist of such disjunctions. Since every sentence of propositional logic is logically equivalent to a conjunction of disjunctive literals, a sentence expressed as a conjunction of disjunctions of literals is said to be in conjunctive normal form (CNF).
Every sentence can be transformed into a CNF sentence using the following steps:
1. Eliminate ↔ replacing P ↔ Q with (P→Q) ∧ (Q →P)
2. Eliminate → replacing P → Q with ¬ P ∨ Q.
3. CNF requires ¬ should appear only in literals, so we move ¬ in wards by repeated application of following equivalences given in table 6.2.
¬(¬ P) ≡ P double-negation elimination
¬ (P ∧ Q) ≡ (P ∨ ¬ Q) De Morgan
¬(P ∨ Q) ≡ ¬ (P ∧ ¬ Q) De Morgan
4. Apply distributive law distributing ∨ over ∧, whenever possible using a sentence in k-CNF has exactly R literals per clause.
Another example from real time environment illustrates the use of resolution theorem for reasoning with propositional logic.
Example 2:
Consider the following knowledge base:
1. If the-humidity-is-high or the-sky-is-cloudy.
2. If the-sky-is-cloudy then it-will-rain.
3. If the-humidity-is-high then it-is-hot.
4. It-is-not-hot.
and the goal: It-will-rain prove by resolution theorem that the goal is derivable from the knowledge base.
Proof:
Let us first denote the above clauses by the following symbols.
p = the-humidity-is high, q = the-sky-is-cloudy, r = it-will-rain, s = it-is-hot.
The CNF form of the above clause thus become-
1. p ∨ q
2. ¬ q ∨ r (after applying theorem 10)
3. ¬ p ∨ s (after applying theorem 10)
4. ¬ s
5. ¬ r
and the negated goal = ¬ r. The set of statements; S, thus includes all these 5 clauses in Normal Form. When all the clauses are connected through connector ∧ they are called in CNF and conjugated terms for the set S. For example
Now by resolution algorithm, we construct the graph of Fig. 6.5. Since it terminates with a null clause the goal is proved.
Summary: Resolution in Propositional Logic:
To prove kB |= α, show that kB ∧ ¬ α is unsatisfiable. Resolution uses k, B, ¬ α in CNF. It combines two clauses to make new one. The inference process continues until empty clause is derived (contradiction) or no new sentences can be created. Briefly
PL resolution rule is
Resolution is sound and complete.
Soundness and Completeness of Resolution in Propositional Logic:
Soundness and completeness are two major issues of the resolution algorithm. While soundness refers to the correctness of the proof procedure, completeness implicates that all the possible inferences can be derived by using the algorithm. Formal definitions of these are presented here for convenience.
A proof process is called sound, if any inference a has been proved from a set of axioms S by a proof procedure, i.e. S l- α, it follows logically from S, i.e., l- α,
A proof process is called complete, if for any inference a which follows logically from a given set of axioms S, i.e. S l- α,, the proof procedure can prove a, i.e. l- α,.
The term logically follows, quite common in logic should be properly understood. For expression x-logically follows from S means it must be true for every interpretation which satisfies the original set of expressions S. This means that any new predicate expression to the existing must be true in that world as well as in any other interpretation which that set of expressions may have.
1. Theorem: The Resolution Theorem is Sound:
Proof:
Given a set of clauses of S and a goal α. Suppose we derived a from S by the resolution theorem. By our usual notation, we thus have S├ α. We want to prove that the derivation is logically sound, i.e. S├ α. Let us prove the theorem by the method of contradiction. So, we presume that the consequents ├ α is false, which in other words means S ├ ¬ α,.
Thus ¬∝ is satisfiable. To satisfy it, we assign truth values (true/false) to all proposition which are used in a. We now claim that for such assignment, resolution of any two clauses from S will be true. Thus, the resulting clause even after exhaustion of all clauses through resolution will not be false. Thus, S ├ α is a contradiction. Hence, the assumptions S ├ ¬ α is false and consequently, S ╞ α is true.
2. Theorem: The Resolution Theorem is Complete:
Search algorithms (such as iterative deepening) are complete in the sense that they will find any reachable goal, but if the available inference rules are inadequate then the goal is not reachable no proof exists which uses only those inference rules.
Any complete search algorithm through resolution can derive any conclusion entailed by any knowledge base. But this is not without a caveat − resolution is complete only in a limited sense. Given a statement P to be true we cannot generate the consequence P v Q. However, through the development of resolution we can answer the query whether P v Q is true.
This is called refutation Completeness meaning that resolution can always be used to either confirm or refute a sentence, but it cannot be used to enumerate true sentences. Resolution operates only when the statements are represented in the standard form. It produces proof by Refutation, negation of goal statement produces a contradiction with the known statements.
The term logically follows is a bit confusing. It does not mean that X is deduced from or even that it is deducible from S. It simply means that a is true for every (potentially infinite) interpretations which satisfies S, though infinite interpretations are not possible.
Instead, inference rules provide a computationally feasible way to determine when an expression a component of an interpretation, logically follows for that interpretation. The concept “logically follows” provides a formal basis for proofs of the soundness and correctness of inference rules.
An inference rule is essentially a mechanical means of producing new predicate calculus statements from other sentences. That is inference rules produce new sentences based on the syntactic form of given logical assertions. When every sentence X produced by an inference rule operating on a set S of logical expressions logically follows from S, the inference rule is said to be sound.
If the inference rule is able to produce every expression which logically follows from S, then it is said to be complete. Modus Ponens, and resolution are examples of inference rules which are sound and when used with certain appropriate strategies complete. Logical inference systems generally use sound reasons of inference, though heuristic reasoning and common sense reasoning relax this req
Limitations of Propositional Logic:
Consider a classic argument:
All men are mortal
Socrates is a man
... Socrates is mortal.
We know that the great philosopher of the world, socrates has since died so this argument is a valid one syllogism. Can we prove the validity using propositional logic.
To find the answer, write this argument as a scheme:
p = All men are mortal
q = Socrates is a man
r = Socrates is mortal,
and so argument schema is:
We may note that there are no logical connectives in the premises (propositions) or conclusion so each premise and each conclusion must have a different logical variable. Also, propositional logic has no provision for quantifiers and so there is no way to represent the quantifier “all” in the first premise. All the three, two premises and the conclusion, in the argument schema need different three independent variables.
To check the validity of this argument, we consider the truth table 6.4 of three independent variables, each one has value T or F.
The second row (indexed by arrow →) of this truth shows the argument to be invalid because the premises are true while the conclusion is false. The invalidity of this argument should not be interpreted as meaning that the conclusion is incorrect. The invalidity, however, does-convey that the under propositional logic the given argument can not be proved.
The argument can be proved valid over if the internal structure of the premises of the argument, attributing some meaning to “all” and recognizing “men” as plural of man. But this internal examination of the premises is not allowed neither by the propositional logic nor by syllogisms.
The only valid sollogistic form of the premise is:
Major premise:
If socrates is a man, then socrates is mortal.
Minor premise:
Socrates is a man.
Conclusion ... , Socrates is mortal
Let p = Socrates is a man
q = Socrates is mortal
The argument becomes:
which is a valid sollogistic form of modus ponens. (Sollogism is a deductive scheme of a formal argument consisting of a major and a minor promise and conclusion).
Another Example:
All horses are animals conclusion therefore, the head of a horse is the head of an animal. Intuitively this argument is correct yet it cannot be proved under propositional logic. But it can be proved under predicate logic as a logical consequence of p and q. The natural inference, Socrates being mortal derives itself from the intuitive nature of the sentences selected.
The propositional logic fail to capture the relationship between any individual being a man and that individual being mortal. Thus, we really need variables and quantification unless we are willing to write separate statements about the mortality of every known man.
Thus, propositional logic lacks in expressiveness which is one of the requirements for a good knowledge representation scheme. Propositional logic is too ‘coarse’ to easily describe properties of objects and lacks the structure to express relations which exist among two or more entities.
Further, propositional logic does not permit us to make generalized statements about classes of similar objects, and lacks the structure to express relations which exist between two or more entities. These are serious limitations when reasoning about real world entities.
Limitations of Propositional Logic:
Consider a classic argument:
All men are mortal
Socrates is a man
... Socrates is mortal.
We know that the great philosopher of the world, socrates has since died so this argument is a valid one syllogism. Can we prove the validity using propositional logic.
To find the answer, write this argument as a scheme:
p = All men are mortal
q = Socrates is a man
r = Socrates is mortal,
and so argument schema is:
We may note that there are no logical connectives in the premises (propositions) or conclusion so each premise and each conclusion must have a different logical variable. Also, propositional logic has no provision for quantifiers and so there is no way to represent the quantifier “all” in the first premise. All the three, two premises and the conclusion, in the argument schema need different three independent variables.
To check the validity of this argument, we consider the truth table 6.4 of three independent variables, each one has value T or F.
The second row (indexed by arrow →) of this truth shows the argument to be invalid because the premises are true while the conclusion is false. The invalidity of this argument should not be interpreted as meaning that the conclusion is incorrect. The invalidity, however, does-convey that the under propositional logic the given argument can not be proved.
The argument can be proved valid over if the internal structure of the premises of the argument, attributing some meaning to “all” and recognizing “men” as plural of man. But this internal examination of the premises is not allowed neither by the propositional logic nor by syllogisms.
The only valid sollogistic form of the premise is:
Major premise:
If socrates is a man, then socrates is mortal.
Minor premise:
Socrates is a man.
Conclusion ... , Socrates is mortal
Let p = Socrates is a man
q = Socrates is mortal
The argument becomes:
which is a valid sollogistic form of modus ponens. (Sollogism is a deductive scheme of a formal argument consisting of a major and a minor promise and conclusion).
Another Example:
All horses are animals conclusion therefore, the head of a horse is the head of an animal. Intuitively this argument is correct yet it cannot be proved under propositional logic. But it can be proved under predicate logic as a logical consequence of p and q. The natural inference, Socrates being mortal derives itself from the intuitive nature of the sentences selected.
The propositional logic fail to capture the relationship between any individual being a man and that individual being mortal. Thus, we really need variables and quantification unless we are willing to write separate statements about the mortality of every known man.
Thus, propositional logic lacks in expressiveness which is one of the requirements for a good knowledge representation scheme. Propositional logic is too ‘coarse’ to easily describe properties of objects and lacks the structure to express relations which exist among two or more entities.
Further, propositional logic does not permit us to make generalized statements about classes of similar objects, and lacks the structure to express relations which exist between two or more entities. These are serious limitations when reasoning about real world entities.