Axioms asserting that the neighbor counts are correct:
- Count of 0:
- "A0": A − has − 0 ⇒ B − safe ∧ G − safe
- ...
- "H0": H − has − 0 ⇒ G − safe ∧ J − safe ∧ P − safe
- ...
- "Z0": Z − has − 0 ⇒ Y − safe
- Count of 1:
- "A1": A − has − 1 ⇒ B − safe ∧ G − unsafe ∨ B − unsafe ∧ G − safe
- ...
- "H1": H − has − 1 ⇒ G − safe ∧ J − safe ∧ P − unsafe ∨ G − safe ∧ J − unsafe ∧ P − safe ∨
- G − unsafe ∧ J − safe ∧ P − safe
- ...
- "Z1": Z − has − 1 ⇒ Y − unsafe
- Count of 2:
- "A2": A − has − 2 ⇒ B − unsafe ∧ G − unsafe
- ...
- "H2": H − has − 2 ⇒ G − safe ∧ J − unsafe ∧ P − unsafe ∨ G − unsafe ∧ J − safe ∧ P − unsafe ∨
- G − unsafe ∧ J − unsafe ∧ P − safe
- ...
There aren't any such axioms for locations with only one neighbor.
- Count of 3:
- "H3": H − has − 3 ⇒ G − unsafe ∧ J − unsafe ∧ P − unsafe
- ...
There aren't any such axioms for locations with only one or two neighbors.
Axioms asserting that the propositions for counting neighbors are consistent:
- A − has − 0 ∨ A − has − 1
- A − has − 0 ⇒¬A − has − 1
- A − has − 1 ⇒¬A − has − 0
- B − has − 0 ∨ B − has − 1 ∨ B − has − 2
- B − has − 0 ⇒¬B − has − 1 ∧¬B − has − 2
- B − has − 1 ⇒¬B − has − 0 ∧¬B − has − 2
- B − has − 2 ⇒¬B − has − 0 ∧¬B − has − 1
- ...
- H − has − 0 ∨ H − has − 1 ∨ H − has − 2 ∨ H − has − 3
- H − has − 0 ⇒¬H − has − 1 ∧¬H − has − 2 ∧¬H − has − 3
- H − has − 1 ⇒¬H − has − 0 ∧¬H − has − 2 ∧¬H − has − 3
- H − has − 2 ⇒¬H − has − 0 ∧¬H − has − 1 ∧¬H − has − 3
- H − has − 3 ⇒¬H − has − 0 ∧¬H − has − 1 ∧¬H − has − 2
- ...
Axioms asserting that the safety propositions are consistent:
- A − safe ⇒¬A − unsafe,
- ¬A − safe ⇒ A − unsafe,
- ...
- Z − safe ⇒¬Z − unsafe,
- ¬Z − safe ⇒ Z − unsafe.
This set of axioms is not quite complete, as explored in an exercise (Exercise 2.5.13).
As mentioned, it is redundant to have both A − safe and A − unsafe as propositions. Furthermore, having both allows us to express inconsistent states (ones that would contradict the safety axioms). If implementing this in a program, you might use both as variables, but have a safety-check function to make sure that a given board representation is consistent. Even better, you could implement WaterWorld so that these propositions wouldn't be variables, but instead be calls to a lookup (accessor) functions. These would examine the same internal state, to eliminate the chance of inconsistent data.
Using only truejfalse propositions; without recourse to numbers makes these domain axioms unwieldy. Later, we'll see how Relations and Syntax and semantics of quantifiers help us model the game of Water-World more concisely.
- 1615 reads
