Axioms asserting that the neighbor counts are correct:
-
Count of 0:
- “A0”:
A-has-0⇒B-safe∧G-safe A-has-0
B-safe G-safe
- …
- “H0”:
H-has-0⇒G-safe∧J-safe∧P-safe H-has-0
G-safe J-safe P-safe
- …
- “Z0”:
Z-has-0⇒Y-safe Z-has-0
Y-safe
-
Count of 1:
- “A1”:
A-has-1⇒B-safe∧G-unsafe∨B-unsafe∧G-safe
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 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 Z-has-1
Y-unsafe
-
Count of 2:
- “A2”:
A-has-2⇒B-unsafe∧G-unsafe
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
H-has-2
G-safe J-unsafe P-unsafe
G-unsafe J-safe P-unsafe
G-unsafe J-unsafe P-safe
- …
-
Count of 3:
- “H3”:
H-has-3⇒G-unsafe∧J-unsafe∧P-unsafe H-has-3
G-unsafe J-unsafe P-unsafe
- …
Axioms asserting that the propositions for counting neighbors
are consistent:
- A-has-0∨A-has-1A-has-0 A-has-1
- A-has-0⇒¬A-has-1A-has-0
A-has-1
- A-has-1⇒¬A-has-0A-has-1
A-has-0
- B-has-0∨B-has-1∨B-has-2B-has-0 B-has-1 B-has-2
- B-has-0⇒¬B-has-1∧¬B-has-2B-has-0
B-has-1
B-has-2
- B-has-1⇒¬B-has-0∧¬B-has-2B-has-1
B-has-0
B-has-2
- B-has-2⇒¬B-has-0∧¬B-has-1B-has-2
B-has-0
B-has-1
- …
- H-has-0∨H-has-1∨H-has-2∨H-has-3H-has-0 H-has-1 H-has-2 H-has-3
- H-has-0⇒¬H-has-1∧¬H-has-2∧¬H-has-3H-has-0
H-has-1
H-has-2
H-has-3
- H-has-1⇒¬H-has-0∧¬H-has-2∧¬H-has-3H-has-1
H-has-0
H-has-2
H-has-3
- H-has-2⇒¬H-has-0∧¬H-has-1∧¬H-has-3H-has-2
H-has-0
H-has-1
H-has-3
- H-has-3⇒¬H-has-0∧¬H-has-1∧¬H-has-2H-has-3
H-has-0
H-has-1
H-has-2
- …
Axioms asserting that the safety propositions are consistent:
- A-safe⇒¬A-unsafeA-safe A-unsafe,
- ¬A-safe⇒A-unsafeA-safe A-unsafe,
- …
- Z-safe⇒¬Z-unsafeZ-safe Z-unsafe,
- ¬Z-safe⇒Z-unsafeZ-safe Z-unsafe.
This set of axioms is not quite complete, as explored in
an exercise.
As mentioned, it is redundant to have both
A-safeA-safe and A-unsafeA-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 true/false propositions;
without recourse to numbers makes these domain axioms unwieldy.
Later, we'll see how
relations and
quantifiers
help us model the game of WaterWorld more concisely.
