Predicate calculus and computing
predicates. In order to unify these two predicates, we have to find a substitution that turns the two predicates into the same form. The substitution that we would use for the example above would be υ = ρ and α = f ( υ )), and the predicates produced would be as follows: [3]
¬ β ( ρ, f ( υ ))
and
β ( ρ, f ( υ ))
This would then allow the two clauses to be resolved, providing they satisfy the other conditions needed for resolution to take place. If the formula contains any ∀ quantifiers, the symbols are ‘ removed ’ as each and every variable is understood to be universally quantified, so it increases readability by reducing the number of unnecessary symbols. However, if the formulas contain any ∃ quantifiers, they need to be removed using a process called skolemization . A formula may be converted into Skolem normal form while not changing its satisfiability. The formula that arises as result of skolemization may not be equivalent to the original one, but they are equisatisfiable i.e., it is only satisfiable if and only if the original one is satisfiable. [6] For example, take the formula ∀ ν ∃ α ∀ ρ L ( ν , α , ρ ), with L being an arbitrary predicate. I have kept the universal quantifiers to aid readability and to help explain the process better. It is clear that this formula is not in Skolem normal form because the statement contains the ∃ quantifier. We shall replace the variable α with the function f ( ν ). The new function f is called the Skolem function and the whole term, f( ν ) is called the Skolem term. The resulting formula is therefore ∀ ν ∀ ρ L ( ν , f ( ν ), ρ ). While performing skolemization, it is important to consider the scope of the different operators. When creating the Skolem term, we have only included the variable ν , and not the variable ρ . This is because the ∃ quantifier was in the scope of ∀ ν , but not in the scope of ∀ ρ . The scope of the different operators flows to the right side of the operator in question. Now we have a formula which is in Skolem normal form, we can continue resolving each pair of clauses until a contradiction is reached. If a contradiction is reached, the formula is proved; if it cannot be reached, the formula cannot be proved using the current axioms. In order to show the power of resolution, I will use the famous wolf, goat and cabbage problem [7] as an example. The problem is simple: a man wants to take a wolf, goat and cabbage across a river. He has rented a boat which can only carry himself and one other object. He cannot leave the wolf with the goat on any side, because the wolf will eat the goat; and he cannot leave the cabbage with the goat on any side, because the goat will eat the cabbage. How can the man get all the items to the other side of the river? We can use the predicate P ( m , w , g , c ) with the variables representing the man, wolf, goat and cabbage respectively. [8] These variables will take a value of 0 or 1. A value of 0 will mean the object is on the other end (far side) of the river, whereas a value of 1 will mean the object is on the starting end (near side) of the river. For example, the predicate P (1, 0, 0, 1) is false, or cannot be true, because the wolf and goat cannot be alone together as the wolf would eat the goat. We can also use the ‘ same value ’ predicate, S ( μ , ν ). This predicate will be true if μ and ν have the same value, in other words, if the objects are on the same side of the river. Finally, we can use the ‘ opposite value ’ predicate O ( α ) which will return 1 if α is 0, or 0 if α is 1. This will allow us to check if objects are on different sides of the river. It is worth noting that the names of these predicates are entirely made up, and their functionality were made to fit the riddle.
From the instructions given to us in the original problem, we can create 9 axioms that we can use for resolution.
228
Made with FlippingBook - Online catalogs