RESOLUTION IN THE PROPOSITIONAL CALCULUS
A New Rule of Inference : Resolution
Resolution is a procedure that produce's proofs by refutation or contradiction.
Resolution leads to refute a theorem proving technique for sentence in propositional logic and first order logic.
- Resolution is rule of inference.
- Resolution is a computerized theorem prover
- Resolution is so far only defined for propositional logic. The strategy is that the resolution techniques of propositional logic can be adopted in Predicate logic.
Clauses as wffs
Either an atom or negation of atom is called as literal. If it is an atom we call it as positive literal. If it is negation of atom we call it as negative literal. A set of literal is known as a clause. This set is formed by disjunction of all the literals, hence a clause is also known as special case of wff.
Resolution on Clauses
When we have our clauses in CFL, resolution is a very easy algorithm. The resolution works by refutation. First of all, it adds the negative of the theory to clause database. Then, in each step you combine (resolve) two parent clauses and fit a new one. The new clause represents the ways that the parent clauses can interact. Consider the example.
winter ∨ summer
ㄱsummer ∨ warm
Remember that this means that both the clauses are correct. Since in CFL, the clauses are co-joined implicitly. We know that for every literal P, only of P or ㄱP is true. So we know that summer or ㄱsummer is true every where. If summer is true then ㄱ summer is false and thus warm is true. If summer is false, then we can conclude that winter is true. Thus from these two clauses we can conclude that.
winter ∨ warm
This is how the resolution works. It takes clauses that each contains the same literals in different senses, in our example, summer which is positive in first clause and negative in .the second, the result clause, which we call resolvent is obtained by containing the literals in original clauses except the common literal. If the resolvent is an empty clause, then we have come by a contradiction and the procedure half.
If there is a contradiction, this algorithm will find it, of course, if there is not contradiction, it is possible that the process never terminates.
So, far, we only considered resolution in propositional logic. In the predicate logic, this algorithm will be more complex, because we will have to handle variables and assign them correct values. The theoretical basis of the resolution procedure in predicate calculus in brand is theorem which tells the following,
- To show that a set of clauses S is satisfactory. It is necessary to consider only interpretations over particular set, called the herbrand universe of S.
- A set of clauses S in unsatisfactory if and only if a finite subset of group instance A (in which all brand variables have handed a value substituted for them) of S is satisfactory.
Soundness of Resolution
Two clauses called parent clauses are compared (resolved) yielding a new clause that has been inferred from them.
winter ∨ summer = ㄱwinter ∨ cold
If winter → T then ㄱwinter → F
∴ cold must be T
So, that
ㄱwinter ∨ cold is true
If ㄱwinter is T, winter → F,
So that,
winter ∨ summer → T
winter ∨ summer ㄱwinter cold.
So this can be deduced as summer ∨ cold.
Resolution operates by taking two clauses that each contain the same literal. For example, winter. The literal must occur in +ve form in one clause and -ve form in the other. The resolvent is obtained by combines all if the two parent clauses except the ones that cancel.
winter ∧ ㄱ winter will produce empty clause.
