Our domain is simply the set of all board locations. This set can be arbitrarily large even infinite!
The board configuration is given by the binary "neighbor" relation nhbr.
The next relations correspond directly to the Propositions in the propositional logic model.
- Whether or not a location contains a pirate: safe. This is a unary relation.
- ASIDE: We choose not to include a redundant relation unsafe.
- Unary relations indicating the number of neighboring pirates: has0, has1, has2, and has3.
ASIDE: Thus, we have our restriction to three unsafe neighbors. This will also be reflected in our domain axioms below. See also this problem (Exercise 3.5.1) for a discussion of how to avoid this restriction.
In addition, to have encode the domain axioms for an arbitrary domain, we also need an equality relation over our domain of locations. As is traditional, we will use infix notation for this relation, for example, x = y. Furthermore, we will allow ourselves to write x = y as shorthand for ¬ (x = y). Thus, we do not need a distinct inequality relation.
Note that these relations describe the state of the underlying board the model and not our particular view of it. Our particular view will be reflected in which formulas we'll accept as premises. So we'll accept has2 (A) as a premise only when A has been exposed and shows a 2.
- 1057 reads
