Predicate calculus and computing
¬ P ( α , α , μ , ν ) ∨ S ( μ , ν ) ∨ P ( O ( α ), O ( α ), μ , ν )
[ * P (0, 0, 1, 0) ]
¬ S ( α , O ( α ))
μ = O ( α )
ν = α
¬ P ( α , α , O ( α ), α ) ∨ S ( O ( α ), α ) ∨ P ( O ( α ), O ( α ), O ( α ), α )
R
¬ P ( α , α , O ( α ), α ) ∨ P ( O ( α ), O ( α ), O ( α ), α )
α = 0
¬ P (0, 0, 1, 0) ∨ P (1, 1, 1, 0)
R
¬ P ( α , μ , α , ν ) ∨ P ( O ( α ), μ , O ( α ), ν )
* P (1, 1, 1, 0)
μ = α
ν = O ( α )
¬ P ( α , α , α , O ( α )) ∨ P ( O ( α ), α , O ( α ), O ( α ))
α = 1
¬ P (1, 1, 1, 0) ∨ P (0, 1, 0, 0)
R
* P (0, 1, 0, 0)
The diagram above shows the resolution stages of the next two steps of the river problem. To begin, we used axiom 3 and substituted μ = O ( α ) and ν = α . We had to use two substitutions so that we could successfully resolve the resulting statement with axiom 2 and remove the ‘ opposite value ’ predicate. We then substituted α = 0 into the statement which we then subsequently resolved against the predicate P (0, 0, 1, 0) which resulted in a derived predicate of P (1, 1, 1, 0) which is the next step towards the solution. In English, this predicate means that the man has rowed the wolf to the other side of the river. We then used axiom 4 again and substituted μ = α and ν = O ( α ) into the statement. This time, we did not need to resolve as we could directly resolve the resulting statement, after a substitution of α = 1, with the predicate P (0, 1, 0, 0), as we had a predicate with its negated version. Once these statements cancel out, we are left with a single predicate, P (0, 1, 0, 0), which is the fourth step towards the finished solution. In English, this predicate means that the man has returned with the goat to the initial side of the river.
The next two resolutions, to get the fifth step towards the solution, is shown below.
231
Made with FlippingBook - Online catalogs