Marc Denecker, Daniele Theseider Dupré, and Kristof Van Belleghem:

An Inductive Definition Approach to Ramifications.

Summary of the article.


This summary is also available in postscript.

This paper describes a new approach to the ramification problem. The approach consists of several contributions.

First of all we show that the standard view on causal laws as rules serving to restore the integrity of state constraints is too restrictive. We argue that causal laws essentially represent the propagation of physical or logical forces through a dynamic system, and that state constraints may be a by-product of this propagation process but that this is not necessarily the case. Therefore we introduce causal laws as pure effect propagation rules independent of state constraints, and define a transition function only dependent on the causal rules which maps each state and set of actions to a resulting state.

Second, we argue that in order to obtain a natural and modular representation of the effect propagation process, the language of causal rules needs to allow for recursion to model mutually dependent effects, as well as for negation to model effects which propagate in the absence of other effects. To define a semantics for complex effect theories involving both negative and cyclic dependencies between effects, we observe that a fundamental property of the process of effect propagation is that it is constructive: effects do not spontaneously appear without an external cause; each effect must be caused by a preceding effect and in practice effects are generated in a bottom-up way. To adequately model this constructive nature of physical change propagation, we base the semantics of the formalism on the principle of inductive definition, the main mathematical constructive principle.

We use a generalised inductive definition principle, which in fact generalises several different approaches. For theories without recursion, the semantics we propose coincides with completion (and can as such be seen as a generalisation of explanation closure approaches). For theories without negation, the semantics coincides with positive inductive definition semantics and standard circumscription (which has also received a lot of attention in research on the frame problem). For stratified theories the semantics coincides with iterated inductive definitions and with the perfect model semantics for stratified logic programs. In the most general case the proposed operator used in the fixpoint calculation coincides with the well-founded operator in logic programming.

The proposed semantics allows to deal with any effect theories without syntactic restrictions on cycles or negations. As a consequence, syntactically correct effect theories exist which do not have a constructively well-defined model. In particular this is the case for effect theories containing actual cycles over negation, e.g. when the existence of each of two effects depends on the other effect's absence. The physical systems corresponding to such effect theories are rare, and those that exist (those deliberately constructed to yield such an effect theory) exhibit unstable behaviour. But the distinction between good and bad effect theories can not be made based on syntactical properties. Our semantics is such that it detects and marks bad effect theories while it assigns a unique transition function to good, constructive, effect theories, including some that appear syntactically problematic.

A third contribution is the introduction of so-called complex effect rules which provide a higher-level description of effect propagations. These complex effect rules allow to state that it is the change in truth value of a complex fluent formula, rather than the change of a single fluent, which triggers certain effect propagations. Complex effect rules map to sets of low-level definition rules. We have observed that one form of complex effect rule is sufficiently expressive to model all kinds of temporal reasoning examples known to us, which also suggests that the corresponding low-level rules only occur in particular combinations in practice. The high-level effect rules offer a much more natural and compact way of describing ramifications than the low-level rules. In particular they prove to be very effective for modeling cumulative or canceling effects of simultaneous actions.

An essential property of the semantics, which distinguishes it from several other approaches, is that it is deterministic: for a given effect theory, any combination of a state and set of actions yields a unique set of causations and hence a unique resulting state (sometimes an inconsistent one, in which case the set of actions is not allowed in the given starting state). In our view nondeterminism should be explicitly represented if it is intended, hence we do not allow nondeterminism to arise from special combinations of otherwise deterministic rules. We do describe an extension of effect rules which allows for a limited form of nondeterminism, in that the rules can state that some effects are allowed, but not forced, to occur. This approach has been further extended to more expressive nondeterministic rules, but this issue is beyond the scope of the current paper.

Our approach is presented independent of a specific time structure or formalism, such as Situation Calculus,  A  or Event Calculus. We briefly discuss how it can be embedded in these different time structures.

We compare our approach to related work in the literature. In particular we show a correspondence between our nondeterministic effect rules and the causal rules proposed by Thielscher. Differences are, apart from the nondeterministic aspect, especially the different view on delays in effect propagations.