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:
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:
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:
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.