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?

The 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 workings of the algorithm, could someone explain it to me?

function PL-RESOLUTION(KB,α) returns true or false inputs: KB, a 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 contain the empty clause then 

return true 

new <--- new ∪ resolvents 

if new ⊆ clauses then 

return false 

clauses <---- clauses ∪ new

Answer 1

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

• Apple is red
• If something is red Then this something is sweet

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

• R('apple')

• R(X) -> S(X)

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

Calculating resolvents step in your programs delete two opposite facts:

• a & ¬a -> empty. 

• a('b') & ¬a(x) v s(x) -> S('b')

Note that in the second fact, the variable x substituted with actual value 'b'.

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

• CLAUSE1 = R('apple')

• CLAUSE2 = ¬R(X) v S(X)

• Goal? = ¬S('apple')

The algorithm works as follows:

• Take clause c1 and c2

• calculate resolvents for c1 and c2 gives new clause c3 =  S('apple')

• calculate resolvents for c3 and goal gives us an empty set.

That means our sentence is true. If you can't get an empty set with such resolutions that mean the sentence is false.

If you want to learn Resolution Algorithm then visit this Artificial Intelligence Course.