Posts Tagged ‘Resolution’

PostHeaderIcon Resolution In Predicate Logic

Assume that a set of given statements F and a statement to be proved P:

Algorithm: Resolution In Predicate Logic

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 step 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 resulting clause, called the resolvent, will be the disjunction of all of the literals of both the 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 the other contains T2 and if T1 and T2 are unifiable, then neither T1 nor T2 should appear in the resolvent. We call T1 and T2 complementary literals. Use the substitution produced by the unification to create the resolvent. If there is one pair of complementary literals, only one such pair should be omitted from the resolvent.
4. 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.

If the choice of clauses to resolve together at each step is made in certain systematic ways, then the resolution procedure will find a contradiction if one exists. However, it may take a very long time. There exist strategies for making the choice that can speed up the process considerably as given below.

    1. Resolve only pairs of clauses that contain complementary literals, since only such resolutions produce new clauses that are harder to satisfy than their parents. To facilitate this, index clauses by the predicates they contain, combined with an indication of whether the predicate is negated. Then given a particular clause, possible resolvents that contain a complementary occurrence of one of its predicates can be located directly.

 

    1. Eliminate certain clauses as soon as they are generated so that they cannot participate in later resolutions. Two kinds of clauses should be eliminated: tautologies (which can never be satisfied) and clauses that are subsumed by other clauses (i.e., they are easier to satisfy) and clauses that are subsumed by other clauses (i.e., they are easier to satisfy. For example, P V Q is subsumed by P)

 

  1. Whenever possible, resolve either with one of the clauses that is part of the statement we are trying to refute or with a clause generated by a resolution with such a clause. This is called the set-of-support strategy and corresponds to the intuition that the contradiction we are looking for must involve the statement we are trying to prove. Any other contradiction would say that the previously believed statements were inconsistent.
  2. Resolve with clauses that have a single literal whenever possible. Such resolutions generate new clauses with fewer literals than the larger of their parent clauses and thus are probably closer to the goal of a resolvent with zero terms. This method is called the unit-preference strategy.

PostHeaderIcon Resolution In Propositional 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: Propositional Resolution

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 step 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 the 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.

Suppose we are given the axioms shown in the first column of Table 1 and we want to prove R.First we convert the axioms to clause which is already in clause form. Then we begin selecting pairs of clauses to resolve together. Although any pair of clauses can be resolved, only those pairs that contain complementary literals will produce a resolvent that is likely to lead to the goal of sequence of resolvents shown in figure 1. We begin by resolving with the clause ⱷR since that is one of the clauses that must be involved in the contradiction we are trying to find.

One way of viewing the resolution process is that it takes a set of clauses that are all assumed to be true and based on information provided by the others, it generates new clauses that represent restrictions on the way each of those original clauses can be made true. 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.

Sl. No Given Axioms Converted to Clause Form
1 P P
2 (P˄Q) → R ¬P˅Q˅R
3 (S˅T) → Q ¬S˅Q
4   ¬T˅Q
5 T T

Table 1: Some Facts in Propositional Logic

Figure 1: Resolution In Propositional Logic

Figure 1: Resolution In Propositional Logic

In order for proposition 2 to be true, one of three things must be true: øP, øQ, or R.But we are assuming øR is true. Given that, the only way for proposition 2 to be true is for one of two things to be true: øP or øQ. That is what the first resolvent clause says. But proposition 1 says that P is true, which means that øP cannot be true, which leaves only one way for proposition 2 to be true, namely for øQ to be true. Proposition 4 can be true if either øT or Q is true. But since we now know that øQ must be true, the only way for proposition 4 to be true is for øT to be true. But proposition 5 says that T is true. Thus these clauses to be true in a single interpretation. This is indicated by the empty clause.

Related Articles

Artificial Intelligence – An Overview