A Circumscriptive Formalization of the Qualification Problem

1 Introduction

Two problems that are important in logical formalizations of commonsense reasoning are the frame problem and the qualification problem [McCarthy, 1977; 1980]. While the frame problem has received a lot of attention in the literature in recent years [Lin and Shoham, 1991; Lifschitz, 1991; Kartha and Lifschitz, 1994; Sandewall, 1994; McCain and Turner, 1995; Thielscher, 1997; Giunchiglia et al., 1997; Shanahan, 1997; McIlraith, 2000], the qualification problem has not been studied as carefully(see however the discussion in the section on related work). In this paper, we clearly define what we mean by the qualification problem and introduce a formalization of the problem using nested abnormality theories [Lifschitz, 1995]. This formalization has the advantage that solutions to the frame problem can be incorporated smoothly with the solution to the qualification problem. We also point out problematic aspects of the current approaches to the qualification problem.

The qualification problem [McCarthy, 1980] refers to the difficulty that one has in formalizing an action, because it is difficult or impossible to enumerate all the preconditions that need to be satisfied before the action can be performed. One of the more well known examples that illustrate this problem is the potato in the tailpipe example due to McCarthy. The example is as follows: The action of starting a car results in the engine running. However, there are many implicit preconditions to the action of starting the car, for instance that there is no potato in the tailpipe, the battery is not dead etc. The problem is how to formalize such examples without getting bogged down in the representation of all such preconditions.

Let us examine the example in a little more detail. The action of starting the car (without any qualifications) can be formalized in the situation calculus [McCarthy and Hayes, 1969] as follows:

To take into account various preconditions of the action StartCar, we could modify (1) by adding preconditions to its antecedent as in,

BMD3D0CSD7B4EngineRunningBN D7B5 CM BMD3D0CSD7B4PotatoInTailPipeBN D7B5 ARD3D0CSD7B4EngineRunningBNCACTD7D9D0D8B4StartCarBN D7B5B5BM (2)

However, note that we will be able to include in the language of our axiomatization only a subset of all the preconditions that can affect the outcome of an action, because we cannot foresee all of them. For instance, a factor that could affect the outcome of the action StartCar is the presence (or absence) of a mysterious ray. We would include facts about this ray in the language of our axiomatization only when we are given that this is a relevant fact.

Let us then start by fixing the language. Even then, it would be difficult to foresee all the circumstances (in the language) that can affect an action. Thus the qualification problem does not vanish when the language is fixed, but takes on a slightly different flavor. Now the key question becomes how one can axiomatize the domain of interest in such a way that on learning a new precondition for an action, one is able to incorporate this additional knowledge in a modular fashion in the axiomatization. Note that adding preconditions to the antecedent, as we have done in axiom (2) is not very modular.

Thus, it seems that there are really two related, but distinct aspects to the qualification problem.

1. The problemof how to smoothly incorporate various additions to the language of an axiomatization. The addition into the axiomatization of the facts pertaining to the mysterious ray and its effect on starting the car is an instance of this. Note that here the language of the axiomatization changes as a result of incorporating the change. This aspect of the qualification problem is related to McCarthy's notion of elaboration tolerance 1 [McCarthy,

1 According to McCarthy, "a formalism is elaboration tolerant to

1998]. This aspect is also related to the problem of how to move between axiomatizations (in different languages) that axiomatize a domain in different levels of detail.

1. The problem of how to represent the qualifications to an action, when the language of the axiomatization is fixed. The chief issues here are
2. (a) Whether we can easily incorporate the fact that another circumstance (in the language) qualifies an action without drastically modifying the original axiomatization. For instance, we would like to achieve this by adding a new sentence into the language. Again, this is because of our desire for an elaboration tolerant solution.
3. (b) To see whether the conclusions that are sanctioned formally agree with our intuitions.

Note that the two aspects share a desire for elaboration tolerance, so that a solution for one aspect is likely to contribute to a solution for the other. The current paper deals only with the second of the two aspects of the qualification problem.

The rest of the paper is organized as follows. In the next section, we explain our formalization and give an example of the kind of results that can be proved using our formalization. We then survey related work, summarize the key contributions of this work and point out directions for future work.

2 Formalization

Since our aim is to convey the key ideas, we will explain our formalization via an example, but will indicate at the appropriate places how one would generalize. The example we use is a slightly extended version of the potato in the tailpipe example from [Thielscher, 1996]. The example consists of extending the basic potato in the tailpipe scenario with another action, PutPotato. The result of this action is to put the potato in the tailpipe, unless this action is qualified. This action is qualified if the potato is so heavy that it cannot be lifted.

Following McCarthy [McCarthy, 1986], here are some axioms that capture the scenario:

the extent it is convenient to modify a set of facts expressed in the formalism to take into account new phenomena or changed circumstances".

Here BTCQ is an abnormality predicate that will be minimized. The advantage of this representation is that as we think of new qualifications, they can be easily incorporated into the theory by means of axioms such as (5) and (6).

However, it should be noted that we are rarely interested in solving the qualification problem in isolation. We also need to ensure that the truth values of the fluents do not change without a reason, so that we are able to obtain the intuitively expected results. To see this, let CC be the theory consisting of axioms (3), (4), (5), (6) and (7). Let CC BC be the theory obtained by minimizing BTCQ in CC. We would like CC BC to entail the formula BMBTCQB4PutPotatoBN CB BC B5 and consequently BMD3D0CSD7B4HeavyPotatoBN CB BC B5. Although, intuitively we would then conclude that the fluent HeavyPotato remains false after executing an action in CB BC (since there are no actions that change the truth value of that fluent), CC BC is not strong enough to entail formulae such as BMD3D0CSD7B4HeavyPotatoBNCACTD7D9D0D8B4StartCarBN CB BC B5B5, BMD3D0CSD7B4HeavyPotatoBNCACTD7D9D0D8B4PutPotatoBN CB BC B5B5 etc. This shows that we need to combine a solution to the frame problem with a solution to the qualification problem to enable us to draw the intuitively expected conclusions.

The formalism that we use that helps us in tackling the frame problem and the qualification problem in sequence, without the solutions interfering with each other is the formalism of nested abnormality theories (NATs) [Lifschitz, 1995]. The main feature of NATs is that the effect of a circumscription can be restricted to a part of the theory called a block. Formally, a block is of the form CUBV BD BN BM BM BM BN BV D1 BM A8 BD BN BM BM BM BN A8 D2 CV, where BV BD BN BM BM BM BNBV D1 are function and/or predicate constants and A8 BD BN BM BM BM BNA8 D2 are axioms, possibly containing an abnormality predicate BTCQ. The block corresponds to the circumscription of BTCQ in the theory consisting of A8 BD BN BM BM BM BN A8 D2 , with BV BD BN BM BM BM BNBV D1 allowed to vary. Note that each of A8 BD BN BM BM BM BNA8 D2 itself may be a block.

Formally, the semantics of NATs is defined by a map CV that translates blocks into sentences of the underlying language. We define CV as follows:

where

Here CIRC stands for the circumscription of BTCQ in CVA8 BD CM BM BM BM CM CVA8 D2 with BV BD BN BM BM BM BN BV D1 allowed to vary (see [Lifschitz, 1993a] for the formal definitions). For a sentence A8 that does not include BTCQ, CVA8 is is equivalent to A8.

Since we need to consider the frame problem, we will need to axiomatize the commonsense law of inertia, according to which the truth values of fluents persist unless they are abnormal. Using ideas from [Kartha and Lifschitz, 1995], we formalize this as

and denote it by LI. Here D3D0CSD7 CA is a new predicate, explicitly defined outside the block solving the frame problem as

The role of this predicate for solving the frame problem can be explained roughly as follows-by "factoring away" the result function, we are able to focus attention only on the situation D7 and the situation that we obtain after action CP is performed in D7. For more details and intuitions, the reader is referred to [Kartha and Lifschitz, 1995].

In our formalization, we will formalize the effect of performing an action using the D3D0CSD7 CA predicate. Thus, for instance, the axioms (3) and (4) will become

BMD3D0CSD7B4EngineRunningBN D7B5 CM BMBTCQB4StartCarBN D7B5 AR

D3D0CSD7 CA B4EngineRunningBN StartCarBN D7B5BN (9) BMD3D0CSD7B4PotatoInTailPipeBN D7B5 CM BMBTCQB4PutPotatoBN D7B5 AR D3D0CSD7 CA B4PotatoInTailPipeBN PutPotatoBN D7B5BM (10)

Let CC CT denote the conjunction of axioms that formalize the effect of performing an action using the predicate D3D0CSD7 CA . Then each formula of CC CT is of the syntactic form

or

D4D6CT B7 BYBNBT B4D7B5 CM BMBTCQB4BTBN D7B5 AR D3D0CSD7 CA B4BYBN BTBN D7B5 D4D6CT A0 BYBNBT B4D7B5 CM BMBTCQB4BTBN D7B5 AR BMD3D0CSD7 CA B4BYBN BTBN D7B5BM

where D4D6CT A6 BYBNBT B4D7B5 denotes a finite conjunction of formulas of the form D3D0CSD7B4BYBN D7B5 or BMD3D0CSD7B4BYBN D7B5. In our example, CC CT thus stands for the conjunction of (9) and (10).

Similarly, let CC D5D9CP stand for the conjunction of axioms that formalize the qualifications. Syntactically, these axioms are of the form

D5D9CPD0 BT B4D7B5 AR BTCQB4BTBN D7B5

where D5D9CPD0 BT B4D7B5 is a finite disjunction of conjunction of formulas of the form D3D0CSD7B4BYBN D7B5 and BMD3D0CSD7B4BYBN D7B5. In our example, CC D5D9CP is the conjunction of (5) and (6).

Let CC D3CQD7 stand for the conjunction of axioms that formalize the observations.These axioms are a finite conjuncion of formulas of the formD3D0CSD7B4BYBN CB BC B5 and BMD3D0CSD7B4BYBN CB BC B5. In our case, CC D3CQD7 is (7).

We also introduce the uniqueness of names and domain closure axioms for fluents and actions. For instance, in our example, the uniqueness of names axiom for fluents consists of the following axiom.

EngineRunning BIBP HeavyPotato CM EngineRunning BIBP PotatoInTailPipe CM HeavyPotato BIBP PotatoInTailPipeBM

The domain closure axiom for fluents is

CU BP EngineRunning CN CU BP PotatoInTailPipe CN CU BP HeavyPotatoBM

Let UNA and DCA denote respectively the uniqueness of names axioms and the domain closure axioms for fluents and actions.

We need two technical devices for our axiomatization. Firstly, we need to include an existence of situation axiom ([Baker, 1991]) (denoted ES) that states that corresponding to every set of fluents, there is a situation in which exactly these fluents hold. For our example, the existence of situation axiom consists of the conjunction of

BLD7B4BMD3D0CSD7B4EngineRunningBN D7B5 CM BMD3D0CSD7B4PotatoInTailPipeBN D7B5 CM BMD3D0CSD7B4HeavyPotatoBN D7B5B5BN

and seven other similar formulae asserting the existence of a situation corresponding to other possible truth values of the three fluents.

Secondly, we need to include a formula which states that there is a situation distinct from CB BC where exactly those fluents that hold in CB BC hold. Formally, this formula is

BLD7CJD7 BIBP CB BC CM BKCU CJD3D0CSD7B4CUBN D7B5 AH D3D0CSD7B4CUBN CB BC B5CLCLBM

This formula is denoted ESI (for existence of situation for the initial situation).

We are now ready to give our formalization.

CDBTBN BWBVBTBN CUD3D0CSD7BND3D0CSD7 CA BNCACTD7D9D0D8BN CB BC BM ESBN ESIBN D3D0CSD7 CA B4CUBN CPBN D7B5 AH D3D0CSD7B4CUBN CACTD7D9D0D8B4CPBN D7B5B5BN CUD3D0CSD7 CA BM LIBN CC CT BN CC D5D9CP BN CC D3CQD7 BN CV CVBM

The inner block solves the frame problem. Note that the abnormality predicate that is being circumscribed in this block is the ternary one that occurs in LI, not the binary one occurring in CC CT . Also, CC D5D9CP and CC D3CQD7 do not contain any occurrence of D3D0CSD7 CA and BTCQB4CUBN CPBN D7B5, and hence do not play any role in the circumscription of the inner block 2 . The outer block minimizes the binary BTCQ and solves the qualification problem. The existence of situations axioms ensure that the binary abnormalities are minimized over all situations. The strategy of first solving the frame problem and then the qualification problem can also be found in [Ginsberg and Smith, 1988; Lin and Reiter, 1994].

Let  be the NAT that encodes our example. By entailment relation for , we will mean the circumscriptive entailment relation for NATs (for details, see [Lifschitz, 1995]). As a representative of the kind of results we can prove, we state the following theorem.

Theorem 1 The following set of formulae are entailed by . 1. BMD3D0CSD7B4HeavyPotatoBN CB BC B5 CM BMD3D0CSD7B4PotatoInTailPipeBN CB BC B5. 2. BKCPD7B4D3D0CSD7B4HeavyPotatoBN D7B5 AH D3D0CSD7B4HeavyPotatoBN CACTD7D9D0D8B4CPBN D7B5B5B5BM 3. BMD3D0CSD7B4EngineRunningBN CACTD7D9D0D8B4PutPotatoBN CB BC B5B5.

1. BMD3D0CSD7B4EngineRunningBNCACTD7D9D0D8B4StartCarBN CB BD B5B5 where CB BD BP CACTD7D9D0D8B4PutPotatoBN CB BC B5.

2 This can also be achieved by moving CC D5D9CP and CC D3CQD7 from the inner to the outer block.

The first formula states that the fluents HeavyPotato and PotatoInTailPipe do not hold in the initial situation. This is intuitively expected, since we are given no information as to whether these fluents hold in the initial situation and we would like to assume that these do not hold if we can do so in order to minimize the abnormalities.

The second formula shows that the value of the fluent HeavyPotato does not change as a result of performing an action. Again, this is expected from a solution to the frame problem, as there are no actions that can change the truth value of the fluent HeavyPotato. The third formula follows from the solution of the frame problem for the fluent EngineRunning and (7).

The fourth formula shows that if you put potato in the tailpipe and then start the car, the engine does not start. This is because as a result of performing the first action PutPotato, the second action StartCar becomes qualified.

Without the ES and ESI axioms, we would not be able to obtain the desired conclusions from our formalization. To see this, let us consider a formalization,  BD , of our example that differs from only in that  BD does not include ES and ESI. Define a structure  with the universe of situations, CY  CY D7 defined as CUBCCV, the universe of fluents, CY  CY CU is defined as CUPotatoInTailPipeBN EngineRunningBNHeavyPotatoCV, the universe of actions is defined as CUStartCarBN PutPotatoCV, the interpretation of the predicate D3D0CSD7 defined as D3D0CSD7  BP CUCWPotatoInTailPipeBN BCCXCV and the interpretation of CACTD7D9D0D8, CACTD7D9D0D8  defined as CACTD7D9D0D8  B4BTBN BCB5 BP BC, where BT ranges over the actions. It is easy to check that  is a model of  BD . Hence, we see that  BD BICYBP BMD3D0CSD7B4PotatoInTailPipeBN CB BC B5.

We noted that  entails the formula BMD3D0CSD7B4HeavyPotatoBN CB BC B5. Clearly, this formula will not be entailed if CC D3CQD7 includes the formula D3D0CSD7B4HeavyPotatoBN CB BC B5. This shows that adding an observation does not reduce the set of models of , but changes them. Hence the solution that we present here does not have the restricted monotonicity property [Lifschitz, 1993b] with respect to observation sentences. In general, we do not expect this property to be obeyed by solutions to the qualification problem.

3 RelatedWork

McCarthy [McCarthy, 1986] has suggested using circumscription to solve the qualification problem. The use of BTCQ in our formalization is based on his abnormality predicate, but several ideas in our formalization such as the use of the D3D0CSD7 CA predicate and the use of the existence of situations axiom for solving the qualification problem are new. Also, we consider how to combine a solution to the frame problem with a solution to the qualification problem.

In his brief paper on the qualification problem, Elkan [Elkan, 1995] suggests using a context mechanism for formalizing the qualification problem, but does not present any such formalization. He criticizes a particular formalization of the qualification problem based on default logic on the ground that all the potential qualifications to an action need to made explicit in that formalization. While the criticism is on the mark for the particular formalization, it seems that a formalization in default logic that uses an abnormality predicate will not suffer from this criticism.

Lifschitz [Lifschitz, 1987] formalizes the qualification problem by circumscribing a predicate precond. His formalism is less expressive than ours, since it does not permit one to express that an action is qualified if two fluents are simultaneously true. Also, his formalism is embedded within a causal language known to have difficulties with domain constraints 3 [Baker, 1991].

Thielscher [Thielscher, 1996] claims that global minimization of abnormalities fails to solve the qualification problem. The example that he uses is the one that we have formalized in the previous section as a NAT. The question that Thielscher raises is as to what would happen if we perform the action PutPotato followed by the action StartCar. He claims that if we globally minimize abnormalities, there would be a model where the action PutPotato does not have its intended effect (because that action is qualified) and hence in that model the engine would start after performing the action StartCar.

It should be noted that Thielscher gives only an informal argument for the claim, not a formal proof. His claim seems to be based on the fact that he is considering a propositional language and does not consider abnormalities to have situational arguments. As we have shown, the unintended model does not arise in our formalization.

Thielscher represents qualifications in the form

which indicates that after performing the sequence of actions CP BD BN BM BM BM BN CP D2 , action CP becomes disqualified. To specify such axioms, it is necessary to precompute what the effect of different sequences of actions should be, which is cumbersome. In contrast, our formalization allows us to specify qualifications directly in terms of fluents. However, Thielscher considers the issue of "miraculous qualifications", an issue that we do not consider.

McIlraith [McIlraith, 2000] addresses the frame, ramification and qualification problem within the context of the situation calculus. In contrast to the approach presented in this paper, McIlraith compiles a set of effect axioms and ramification constraints into a set of successor state axioms. It should be noted that such a compilation is possible only when the effect axioms and ramification constraints follow a syntactic restriction. (Theories with such a syntactic restriction are called solitary stratified theories in [McIlraith, 2000]). Whether the approach presented in this paper coincides with that in [McIlraith, 2000] when restricted to the case of solitary stratified theories remains open.

4 Conclusions and Future Work

We have presented a simple formalization of the qualification problem based on NATs and and have shown how to combine a solution to the frame problem with this formalization. We have also argued that this formalization offers several advantages in comparison with existing approaches.

3 By domain constraints, we mean formulae that relate fluents in the same situation. An example of a domain constraint that we may wish to include in our example is D3D0CSD7B4PotatoInTailPipeBN D7B5 AR BMD3D0CSD7B4EngineRunningBN D7B5.

Theorem 1 pertains only to the example presented in this paper. This raises the question as to how we can evaluate the general applicability of the formalization presented here. One way is by proving theorems about what the formalization does and does not entail. For instance, we can prove that the inner block (that solves the frame problem) generates conclusions identical to the ones sanctioned by a BT-like [Gelfond and Lifschitz, 1993] language. Evaluating that the outer block handles qualifications correctly is harder. One approach is to test that the formalization yields intutively expected results on a test suite. A more principled approach is to define a language formalizing intuitions about qualifications and then prove soundness and completeness theorems along the lines of [Kartha, 1993]. Both these approaches are currently being pursued.

One direction for future work is to investigate how the ideas presented in this paper can be generalized to handle domain constraints. In the presence of domain constraints, the situation is more complicated for the following reasons.

• AF The existence of situations axiom needs to be changed, since now, all possible combination of fluents are not consistent.
• AF As pointed out by [Ginsberg and Smith, 1988] and [Lin and Reiter, 1994], some domain constraints can act as constraints on the performability of an action (these are called qualification constraints) whereas some other syntactically indistinguishable domain constraints give rise to indirect effects (these are called ramification constraints).

The first of the above complications can be handled, for instance, by including a block that formalizes a nonmonotonic version of the existence of situations axiom, as in [Kartha and Lifschitz, 1994].

The second difficulty is more serious. If all the constraints are ramification constraints, then solutions to the frame problem shown here can be easily extended (along the lines of [Giunchiglia et al., 1997]). If we have both ramification and qualification constraints, we need to separate the set of constraints into these two sets and consider them separately.

Acknowledgment

I wish to thank the anonymous referees for several suggestions for improving the clarity of this paper.