Predicate calculus and computing
¬ P ( α , μ , ν , α ) ∨ S ( μ , ν ) ∨ P ( O ( α ), μ , ν, O ( α ))
[ * P (0, 1, 0, 0) ]
¬ S ( α , O ( α ))
μ = O ( α )
ν = α
¬ P ( α , O ( α ), α , α ) ∨ S ( O ( α ), α ) ∨ P ( O ( α ), O ( α ), α , O ( α ))
R
¬ P ( α , O ( α ), α , α ) ∨ P ( O ( α ), O ( α ), α , O ( α ))
α = 0
¬ P (0, 1, 0, 0) ∨ P (1, 1, 0, 1)
R
* P (1, 1, 0, 1)
In this set of resolutions, we first used axiom 5 and substituted μ = O ( α ) and ν = α . We then resolved using axiom 2. Substituting α = 0 and resolving with the predicate P (1, 1, 0, 1) gives us the fifth step towards the solution. In English, the predicate tells us that the man has taken the cabbage to the other side of the river. Throughout these resolutions, it is worth nothing that I sometimes resolved the predicates ¬ S ( α , O ( α )) and S ( O ( α ), α ). These predicates are identical, apart from the negation, which makes resolution possible. However, we cannot do this with P (1, 1, 0, 0) and P (0, 0, 1, 1) because the order matters. In the first predicate, α would be equal to 1, in the second, it would be equal to 0. This would lead to an entirely different derived predicate.
The remaining two steps of the solution would be: the man returns to the initial side and then man brings the goat to the other side.
If you continued to resolve the next clauses, you would eventually end up with P (1, 1, 1, 1), where all the animals and the man have made it to the other side of the river. This would of course then be resolved against axiom 8 which would lead to a contradiction.
The basic resolution method generally consists of resolving axioms at random until you obtain a final contradiction. This, of course, is very inefficient when you are dealing with much larger problems because as the number of axioms increase, so does the number of different combinations you can make when resolving. Luckily, two main strategies were created to help make resolution quicker, and to reach the final contradiction in a smaller number of steps. [9] The first is called the unit preference strategy , and it is often used in conjunction with the second strategy, the set-of-support strategy . The unit preference strategy involves resolving clauses that are as short as possible, because this strategy always works it is one of the most used strategies. The second strategy involves using at one least denial clause (or the clauses they derive) in resolution. In the resolution example above, we effectively did both of these strategies, although the axioms that were picked were chosen with the solution in mind and may not entirely follow these strategies.
232
Made with FlippingBook - Online catalogs