How does a Resolution algorithm work for propositional logic?

Question

I haven't been able to understand what the resolution rule is in propositional logic. Does resolution simply state some rules by which a sentence can be expanded and written in another form?
Following is a simple resolution algorithm for propositional logic. The function returns the set of all possible clauses obtained by resolving it's 2 input. I can't understand the working of the algorithm, could someone explain it to me?

  function PL-RESOLUTION(KB,α) returns true or false
     inputs: KB, the knowledge base, a sentence α in propositional logic, the query, a
             sentence in propositional logic 
     clauses <--- the set of clauses in the CNF representation of KB ∧ ¬α
     new <--- {}
     loop do
        for each Ci, Cj in clauses do
            resolvents <----- PL-RESOLVE(Ci, Cj)
            if resolvents contains the empty clause then return true
            new <--- new ∪ resolvents
        if new ⊆ clauses then return false
        clauses <---- clauses  ∪ new                                                                           

Answer 1

It's a whole topic of discussion but I'll try to explain you one simple example.

Input of your algorithm is KB - set of rules to perform resolution. It easy to understand that as set of facts like:

1. Apple is red
2. If smth is red Then this smth is sweet

We introduce two predicates R(x) - (x is red) and S(x) - (x is sweet). Than we can written our facts in formal language:

1. R('apple')
2. R(X) -> S(X)

We can substitute 2nd fact as ¬R v S to be eligible for resolution rule.

Caluclating resolvents step in your programs delete two opposite facts:

Examples: 1) a & ¬a -> empty. 2) a('b') & ¬a(x) v s(x) -> S('b')

Note that in second example variable x substituted with actual value 'b'.

The goal of our program to determine if sentence apple is sweet is true. We write this sentence also in formal language as S('apple') and ask it in inverted state. Then formal definition of problem is:

• CLAUSE1 = R('apple')
• CLAUSE2 = ¬R(X) v S(X)
• Goal? = ¬S('apple')

Algorithm works as follows:

1. Take clause c1 and c2
2. calculate resolvents for c1 and c2 gives new clause c3 = S('apple')
3. calculate resolvents for c3 and goal gives us empty set.

That means our sentence is true. If you can't get empty set with such resolutions that means sentence is false (but for most cases in practical applications it's a lack of KB facts).

Answer 2

Consider clauses X and Y, with X = {a, x1, x2, ..., xm} and Y = {~a, y1, y2, ..., yn}, where a is a variable, ~a is its negation, and the xi and yi are literals (i.e., possibly-negated variables).

The interpretation of X is the proposition (a \/ x1 \/ x2 \/ ... \/ xm) -- that is, at least one of a or one of the xi must be true, assuming X is true. Likewise for Y.

We assume that X and Y are true.

We also know that (a \/ ~a) is always true, regardless of the value of a.

If ~a is true, then a is false, so ~a /\ X => {x1, x2, ..., xm}.

If a is true, then ~a is false. In this case a /\ Y => {y1, y2, ..., yn}.

We know, therefore, that {x1, x2, ..., xm, y1, y2, ..., yn} must be true, assuming X and Y are true. Observe that the new clause does not refer to variable a.

This kind of deduction is known as resolution.

How does this work in a resolution based theorem prover? Simple: we use proof by contradiction. That is, we start by turning our "facts" into clauses and add the clauses corresponding to the negation of our "goal". Then, if we can eventually resolve to the empty clause, {}, we will have reached a contradiction since the empty clause is equivalent to falsity. Because the facts are given, this means that our negated goal must be wrong, hence the (unnegated) goal must be true.