Predicate calculus and computing
¬ P ( α , μ , α , ν ) ∨ P ( O ( α ), μ , O ( α ), ν )
P (0, 0, 0, 0)
x = y = z = 0
¬ P (0, 0, 0, 0) ∨ P (1, 0, 1, 0) R
* P (1, 0, 1, 0)
¬ P ( α , μ , α , μ ) ∨ S ( α , μ ) ∨ P ( O ( α ), μ , α , μ )
¬ S ( α , O ( α ))
μ = O ( α )
¬ P ( α , O ( α ), α , O ( α )) ∨ S ( α , O ( α )) ∨ P ( O ( α ), O ( α ), α , O ( α ))
R
¬ P ( α , O ( α ), α , O ( α )) ∨ P ( O ( α ), O ( α ), α , O ( α ))
α = 1
¬ P (1, 0, 1, 0) ∨ P (0, 0, 1, 0)
R
* P (0, 0, 1, 0)
This diagram shows the first two steps towards the solution. We started with axiom 4 and resolved it with axiom 7 to get the first step. This resulting predicate is P (1, 0, 1, 0) and it shows that the man has taken the goat across the river. We then used axiom 6 and substituted μ = O ( α ) into it. We did this so we could resolve the resulting statement with axiom 2. We could then substitute α =1 and then once again resolve the resulting statement with the predicate P (1, 0, 1, 0) in order to get a resulting statement of P (0, 0, 1, 0) which shows that the man has returned to the initial side, which is the second step towards the final solution.
We can continue resolving to find the next steps towards the solution as shown below. Predicates enclosed in [ ] have already been derived above.
230
Made with FlippingBook - Online catalogs