The Problem of Formalization

The Lemmings player cannot succeed only by reacting directly to the current situation. He must plan ahead, often to the end of the game in which the situation will be very different from the situation when the plan is made. We propose to do this by formalizing the relevant facts in logic and projecting by logical reasoning. I can't prove there is no other way of doing the projection.

Here are some requirements for projection.

1. The ontology (set of entities over which variables range) of the Lemmings world includes lemmings, sets of lemmings, regions, lemming traps, bridges, events including actions, situations, fluents and others. I suppose we should include in the ontology the predicate and function symbols we shall need in the formalism.
2. The events that create, destroy and transform the different kinds of object need special treatment.
3. There must be names for sets of lemmings determined by some properties without the user having to know particular lemmings or even how many there are in the set. Naturally, sets with one element play a special role.

   Maybe the only kind of lemming that has to be treated in sets is walker. Others can be treated individually, because only a few can exist at a time. What is likely to be interesting is the set of walkers in a region. The events that happen to sets of walker as sets need to be distinguished, e.g. a set of walkers can fall into a hole. If each walker in a set falls into a hole, then the set falls into the hole. (If you like old jargon, falling into a hole is an intensive property like temperature.) However, we should be able to draw conclusions about what happens to a set of lemmings without always having to reason about its members. The cardinality of a set is important when a certain resource, e.g. the number of lemmings that can be designated as climbers, is limiting.

4. Natural language discussion of Lemmings suggests that we provide for fluents denoting continuous action, e.g. we should be able to say holds(walking(l,c0,R),s), meaning that lemming l is walking to the right in region c0 in situation s. We will also want to say holds(walking2(l,c0),s), omitting the direction. The former is stopped by encountering a wall, and the latter is not stopped by encountering a wall but is stopped by l becoming a digger or falling into a hole dug by a digger.
5. There must be a way of dealing with parallel processes. ``While I am making group A of lemmings do this, group B is doing that.''
6. Counterfactuals are used in human reasoning about Lemmings, e.g. ``if I had one more bridge-builder I could ''.

The formalism must be elaboration tolerant. A person plays Lemmings with an incomplete knowledge of the properties of the kinds of lemmings and their interaction with features of the scene. An adequate formalization has the property that it can be elaborated to take into account new phenomena by adding statements rather than by completely redoing it.