您在這裡

The domain axioms

18 三月, 2015 - 11:51
Available under Creative Commons-ShareAlike 4.0 International License. Download for free at http://cnx.org/contents/383d4b87-2d7b-454e-99fe-2eaa43eae8ff@20.20

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.