Predicate calculus and computing
1. S ( α , α ) 2. ¬ S ( α , O ( α ))
The statement P ( α , α , μ , ν ) ∨ ¬ S ( μ , ν ) → P ( O ( α ), O ( α ), μ , ν ) creates the next axiom. In English, the statement means that if the man and wolf are on the same side of the river, and the goat and cabbage are on opposite sides of the river, the man can row the wolf to the other side of the river. The axiom created is shown below:
3. ¬ P ( α , α , μ , ν ) ∨ S ( μ , ν ) ∨ P ( O ( α ), O ( α ), μ , ν )
The statement P ( α , μ , α , ν ) → P ( O ( α ), μ , O ( α ), ν ) creates the fourth axiom. In English, the statement means that if the man and goat are on one side of the river, and the wolf and cabbage are on the other side, then the man can row the goat to the other side of the river. The axiom created is shown below:
4. ¬ P ( α , μ , α , ν ) ∨ P ( O ( α ), μ , O ( α ), ν )
The statement P ( α , μ , ν , α ) ∨ ¬ S ( μ , ν ) → P ( O ( α ), μ , ν , O ( α )) creates the fifth axiom. In English, the statement means that if the man and cabbage are on one side of the river, and the wolf and goat are on opposite sides of the river, then the man can row the cabbage to the other side. The axiom created is shown below:
5. ¬ P ( α , μ , ν , α ) ∨ S ( μ , ν ) ∨ P ( O ( α ), μ , ν , O ( α ))
The statement P ( α , μ, α , μ ) ∨ ¬ S ( α , μ ) → P ( O ( α ), μ, α , μ ) creates the sixth and final axiom for the possible ferrying operations. In English, the statement means that if man and goat are on one side of the river and the wolf and cabbage are on the other side of the river, then the man can take himself to the other side. The axiom created is shown below:
6. ¬P ( α , μ, α , μ ) ∨ S ( α , μ ) ∨ P ( O ( α ), μ, α , μ )
The final two axioms show the initial and final state of the problem. It is important to note that axiom 8 is negated. This is important because it will allow us to obtain a contradiction when we eventually arrive at P (1, 1, 1, 1) from resolution. We would have then found the correct solution. These axioms are shown below:
7. P (0, 0, 0, 0) 8. ¬P (1, 1, 1, 1,)
Shown below are a few unifications and resolutions that create part of the solution to the problem. Statements marked with an asterisk represent steps towards the solution and statements marked with an R represent the resolution steps. It is worth mentioning that the axioms chosen were picked with the solution in mind, and normally resolution would be done in a much more random fashion.
229
Made with FlippingBook - Online catalogs