Moderated by Erik Sandewall.

Graham White Simulation, Ramification, and Linear Logic

The article mentioned above has been submitted to the Electronic Transactions on Artificial Intelligence, and the present page contains the review discussion. Click for more explanations and for the webpage of theauthor, Graham White. Overview of interactions N:o Question Answer(s) Continued discussion 1 1.10  Tom Costello 3.10  Graham White   2 3.10  Andreas Herzig 28.10  The author   3 27.3  Anonymous Referee 1 4.4  Graham White 13.4  Anonymous Referee 1 27.4  The Author 28.4  Murray Shanahan 4 27.3  Anonymous Referee 2 4.4  Graham White   5 29.3  Area Editor     6 28.4  Area Editor       Q1. Tom Costello (1.10): Dear Graham On page 2 of your article, "Simulation, Ramification, and Linear Logic" you suggest that effect axioms should have  Sigma1  antecedents and frame axioms  Pi1  antecedents, based on intuitions concerning locality. However, some local properties, such as there being no block in a certain place are expressed as  Pi1  formulas, not as  Sigma1  formulas, e.g.   A(b, ¬ at(b, l))  states that there is no block at location  l . It seems to me that many effect axioms will have preconditions that say that the effect will occur in certain circumstances, unless there is something that prevents it. This is naturally written as a  Pi1  formula. Consider the Blocksworld. One effect axiom there can be written       Ab, l, s [ Ab' [¬ On(b', top(b), s)]  ^                 Ab' [¬ On(b', l, s)]  ^ top(b) =/ l ·->                On(b, l, move(b, l, s))]     The left hand side side of this effect axiom is clearly equivalent to a  Pi1  formula. It seems that many preconditions will have this form. This seems to contradict your intuitions that effect axioms have  Sigma1  antecedents, and that sufficient conditions can be written in  Sigma1 . Yours, Tom Costello A1. Graham White (3.10): Dear Tom, Thanks for your question. It seems to me that I would want first of all to differentiate between your two formulations of the basic objection: i) "some local properties ... are expressed as  Pii  formulas", and ii) "many effect axioms will have preconditions that say that the effect will occur in certain circumstances, unless there is something that prevents it". The first formulation has to do with local properties, which I take to be a fairly general, phenomenological notion; the second is to do with action preconditions, which is a notion internal to certain treatments of the frame problem. I'll deal with the second notion first. My approach doesn't really use action preconditions per se. I don't have anything like a result function: given linear logic terms s and a representing a situation and an action, there may or may not be a valid inference of the form      s, a  |-  s'    where  s'  is also a situation term. So there are, in some sense, implicit action preconditions, but I don't represent them explicitly. I can deal with your example in my framework as follows. We have to introduce constraints on the space of situations, which I can do by having an extra pair of fluents, say good and bad, which say whether situations are physically realisable or not, and also having extra ramification transitions      (on(b, l) × on(b', l) × good)~>(on(b, l) × on(b', l) × bad)    for  b  and  b'  unequal. We now apply the ramification machinery that I described: that is, we look for sequents corresponding to performing the action, followed by a terminating sequence of ramification transitions, such that we eventually end up with a situation of the form  X × good . All of this can be carried out with entirely local data, but the implicit preconditions are as you described. (I'm a bit unsure about the other part of the precondition, which says that you can't pick up a block with another block on top of it. My immediate response to that is "well, I can", but I'm not sure exactly what the impossibility is supposed to be here.) Incidentally, I'm not at all sure about the phenomenological motivation of the concept of precondition. It seems to me that it conflates two quite distinct phenomena: the first is of actions (such as "opening the door") described by what Ryle called "success words", where it doesn't make sense to talk of performing them when they don't succeed. The other is of action descriptions such as "trying to open the door", where the possibility of failure is allowed for, and where we usually also have some intuitions about what happens in the case of failure. As Ryle (and I suppose also Wittgenstein) point out, the second case is rather more complex than the first, and probably needs a more elaborate description than simply giving preconditions. The first is the usual case in a great deal of everyday language, but, by its nature, does not need any explicit talk of preconditions (although one could, presumably, in many cases find implicit preconditions). Your first objection is that many local concepts are in fact  Pii . This may be true, but what surely matters for my analysis is not local concepts per se, but the local concepts that are used in the sort of representation that I am describing. One probably also ought to distinguish between genuine universal quantification and universal quantifications which are, in some way, bounded. Most local concepts would, presumably, only be  Pii  in the latter sense, and it would be a sense corresponding to some natural means of verification -- I check, for example, that there is nothing on my desk by looking at the locations on my desk and verifying that they are all empty (and I can tell that they're empty just by looking at them). I certainly don't do it by finding all of the objects that there are and verifying that none of them is on my desk; and an analysis of "there is nothing on my desk" that reduces it to a  Pi1  of that sort is likely to be epistemologically misleading. I hope this helps, anyway. Graham Q2. Andreas Herzig (3.10): Dear Graham, I appreciate the aims of the paper, viz. the discussion about the logical form and the proof-theoretic account of reasoning about actions as given in sections 1, 2.1.1, 2.4. I think that too little work has been done in the community on such fundamental issues. Basically you propose Linear Logic (LL) as a proof theory to reason about actions, following Girard who claimed from the beginning that LL would be much better suited for reasoning about actions and change than any other logical system. LL people have tried to support that claim, such as Masseron et al. (LNCS 427, 1990) or Bidoit et al. (JLC, 1996). The same has been tried also by people coming from Bibel's linear connection method - see e.g. Bibel's IJCAI'97 invited lecture, as well as work of Fronhofer and Grosse et al. that Bibel cites; see also the subsequent discussion at   http://www.ida.liu.se/ext/etai/actions/deb/bibel/index.html In my opinion all these attemps have failed in the sense that the only thing they can handle within LL is the simplest case: deterministic actions, no state constraints, knowledge about the initial situation only. They didn't succeed in going beyond that without violating the spirit of LL: they all introduced extra concepts that were used to constrain deduction in one way or another. In the present paper it is time which is made explicit in the encoding of reasoning about action problems (section 3, 3rd paragraph). But I would expect time to be implicit in a LL account of reasoning about actions: it is the implication of LL which - if we take Girard seriously - should be able capture the dynamics, and not formulas such as  time(0) ^ occurs(lift)(0) . There seem to be other extra concepts, such as grouping of those sequent rules corresponding to an action (see below). This is my main criticism. What follows are more detailed comments. Sections 2.2. The two-blocks Example 1 is similar to Lifschitz' two switches example, I suppose. (Btw. on p.4, line 8 should be dropped.) I guess circumscription doesn't give the solution, but several ones, one of which you give in the table. (Btw. one  b1  should be  b2  there.) Sections 2.3. I don't understand the difference between Example 1 and Examples 2 and 3. Where does the `support' concept come from? I need more comments here. Section 2.4. The expression "equivalent in first order logic to theory  T , but expressed in  L' " is inaccurate. I don't know whether you refer to logical equivalence in the union of the two languages  L  and  L'  under the translation theory of Table 3, or rather to interpretability as in the end of the subsection. Section 3.2. You claim your rewrite rules for the two blocks theory is `local data', in the sense that they remain valid `if we introduce new types of cause'. But what about introducing an action such as cutting or removing the string between the blocks? Then the rewrite rules `linking' the blocks do not hold any longer. Section 4.1. Wy don't you mention the cut rule here? (you talk about its elimination in the proof of Proposition 1). In the statement of Proposion 1, you don't say what ACI is. If you have cut, how can composition of rewrites be a problem? Cut is just doing that job, viz. chaining sequents. I guess this relates to my main criticism: in order to identify actions in proofs, you must group together sequences of rules related to the same action. This means that there is a new concept that is exterior to LL. (I think the problem of termination of sequences is similar.) Section 4.2. I don't understand how the introduction of modal operators solves the above problem. In the basic rewrite rule of Definition 1, I suppose the LL `times' operator is rather an ACI bullet. I found it difficult to understand the exposition on termination. I suppose termination refers to termination of a rewrite sequence corresponding to an action. In the rule, the notation  A-Ai  has not explained. What is a `state'  Ai ? A2. Graham White (28.10): Dear Andreas, Thank you for your comments on my paper. I'll try to respond in order.   In my opinion all these attemps have failed in the sense that the only thing they can handle within LL is the simplest case: deterministic actions, I can handle non-deterministic actions; all you need is the additive connectives. If you have linear logic terms  a1  and  a2 , each representing an action, then the term  a1 ^ a2  represents the action which nondeterministically executes either  a1  or  a2 .   no state constraints, I haven't talked much about state constraints because I am a little sceptical about the prominent role given to them in the current literature: I do not believe that the ramification behaviour can be given simply by the state constraints. In this respect, my position is somewhat similar to that of Deneker et al. in the article the recently submitted to ETAI (http://www.ep.liu.se/ea/cis/1998/007) However, if you do want state constraints (if, for example, you want to do other things than simply generate the ramification behaviour from them), they can be added to my approach, and I've shown how to treat a simple case in my reply to Tom Costello. However, there are important conceptual (not mathematical) issues to be resolved first: in particular, there is an obvious distinction between state constraints which are required to hold during the ramification process, or only at the end of it.   knowledge about the initial situation only. I can deal with that too. In my "Actions, Ramification, and Linear Modalities", QMW Technical Report no. 749 (1998), at ftp://ftp.dcs.qmw.ac.uk/pub/applied_logic/graham/ramMod.ps, I show that every valid inference in the logic corresponds to an evolution of the system according to the intended semantics, and vice versa; so if we carry out a proof search starting with partial data in either or both of the initial or final situations or in the action (representing the partiality be the appropriate quantifiers:  forall  before the entailment,  exists  after it) then, if that proof search terminates, the corresponding entailment will correspond to a correct evolution of the system.   They didn't succeed in going beyond that without violating the spirit of LL: they all introduced extra concepts that were used to constrain deduction in one way or another. I think you have to distinguish here between "extra concepts ... used to constrain deduction" and genuine extensions of the system. I have tried to show (in "Actions, Ramification, and Linear Modalities") that my extra connectives have both a good proof theory and a semantics.   In the present paper it is time which is made explicit in the encoding of reasoning about action problems (section 3, 3rd paragraph). But I only put the explicit time in to make the example conceptually clearer. You don't need it.   But I would expect time to be implicit in a LL account of reasoning about actions: it is the implication of LL which - if we take Girard seriously - should be able capture the dynamics, and not formulas such as  time(0) ^ occurs(lift)(0) . There seem to be other extra concepts, such as grouping of those sequent rules corresponding to an action (see below). This is, of course, and important point, and I more or less agree with it. However, I want to make one caveat: you do seem to need to represent some notion of synchronisation. That is, you need to say that a particular tensor product of fluent formulae represents a particular situation, and that these are all of the fluents in that situation. Otherwise you can't express universally quantified assertions (for example, if you want to say ``all the blocks are on the table'' in a given situation). I've gone into this in ``Golog and Linear Logic'', QMW Department of Computer Science Technical Report (December 1997), at ftp://ftp.dcs.qmw.ac.uk/applied_logic/graham/golog.ps.   This is my main criticism. What follows are more detailed comments. Sections 2.2. The two-blocks Example 1 is similar to Lifschitz' two switches example, I suppose. (Btw. on p.4, line 8 should be dropped.) I guess circumscription doesn't give the solution, but several ones, one of which you give in the table. (Btw. one  b1  should be  b2  there.) No, circumscription (with the indicated fluents) only gives one solution, and that solution is clearly not the intended one. So it's not similar to Lifschitz' two switches example in that respect.   Sections 2.3. I don't understand the difference between Example 1 and Examples 2 and 3. Where does the `support' concept come from? I need more comments here. Ah. Sorry about that: I forgot to give enough context for the quote from the referee. The point is that you can try to fix up the state constraints by saying that a ball is either supported directly, or hangs from a directly supported ball.   Section 2.4. The expression ``equivalent in first order logic to theory  T , but expressed in  L'  '' is inaccurate. I don't know whether you refer to logical equivalence in the union of the two languages  L  and  L'  under the translation theory of Table 3, or rather to interpretability as in the end of the subsection. Interpretablity. Sorry about the ambiguity.   Section 3.2. You claim your rewrite rules for the two blocks theory is `local data', in the sense that they remain valid `if we introduce new types of cause'. But what about introducing an action such as cutting or removing the string between the blocks? Then the rewrite rules `linking' the blocks do not hold any longer. In that case, of course, we'd have to introduce new fluents, since we don't, in this example, have a representation for whether the string is intact or not, and we'd consequently have to change the rewrite rules somewhat.   Section 4.1. Wy don't you mention the cut rule here? (you talk about its elimination in the proof of Proposition 1). In the statement of Proposion 1, you don't say what ACI is. Well, I can prove cut elimination (in the tech report ``Actions, Ramification, and Linear Modalities''), so the system without cut is equivalent to the system with cut. Cut elimination is important, because, if you have it, you can show that the only proofs of the sequents that encode actions correspond to the changes that those actions produce; that is, it says that the linear logic connectives have their intuitive meaning. This is a theme in a tradition in the proof theory of intuitionism, starting with Martin-Löf; the question is, can you understand the logical connectives simply by their role in proofs? And the answer is, yes you can, if the system satisfies cut elimination: because then we only need finite data to decide whether we can apply a rule or not. But the cut rule breaks this, because we can apply it with any cut formula, which is an unbounded totality. So systems without cut can be understood, in some way, finitely, whereas systems with cut can't.   If you have cut, how can composition of rewrites be a problem? Cut is just doing that job, viz. chaining sequents. We need composition of rewrites in order to be able to prove cut elimination.   I guess this relates to my main criticism: in order to identify actions in proofs, you must group together sequences of rules related to the same action. No, not necessarily; if you look at the examples in ``Actions, Ramification, and Linear Modalities'', you can see that you don't need to group rule applications together like this.   This means that there is a new concept that is exterior to  LL . (I think the problem of termination of sequences is similar.) Section 4.2. I don't understand how the introduction of modal operators solves the above problem. I say more about this in ``Actions, Ramifications, and Linear Modalities'', but I can write more about this if you still find this mystifying.   In the basic rewrite rule of Definition 1, I suppose the LL `times' operator is rather an ACI bullet. I found it difficult to understand the exposition on termination. I suppose it is a bit compressed. I'm intending the paper as a non-technical guide to the more technical results (which are mostly in ``Actions, Ramification, and Linear Modalities''), but I agree with you that some parts of it might have left the technical details out a bit too enthusiastically.   I suppose termination refers to termination of a rewrite sequence corresponding to an action. In the rule, the notation  A-Ai  has not explained. What is a `state'  Ai ? Here you can treat it as a term of the metatheory. We start with atomic terms representing basic fluents; state propositions will then be combinations of them using  otimes  (and you can, in fact, use  oplus  as well, which will give you a notion of disjunctive states). The rewrite operation will then take state propositions to state propositions. Provided you start with atomic terms, and only combine them in the above ways, you can then prove cut elimination. (In ``Actions, Ramifications, and Linear Modalities'' I do it rather differently, and I have a representation within the logic for state terms; but you don't need to do that.) Anyway, I hope this helps. Thanks again for your questions. Graham White Q3. Anonymous Referee 1 (27.3): The following are my answers to the refereeing questions.   1. Are the results of the article, as specified in the summary, of significant interest for researchers in our area? No. The main objective of the paper is to propose a solution to the Frame Problem which satisfies certain properties, which are convincingly argued for. My only but serious concern is that existing solutions seem to satisfy all of the requirements and that the author fails to argue for merits of his approach in comparison. In particular Reiter's theory [1] of generating successor state axioms from simple effect axioms fits perfectly the author's desiderata. And yet this work, which is among today's most cited papers in the area of Reasoning About Actions And Change, the author does not even mention, let alone compare it to his own method. [1] Ray Reiter, "The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression," in: Artificial Intelligence and Mathematical Theory of Computation, Academic Press, 1991.   2. does the full text substantiate the claims made in the summary? Yes.   3. is the text intelligible and concise? Yes.   4. do you know of any previous publication of the same result? No. (But see my answer to Question 1.)   5. are there any other considerations that may affect the decision? No. A3. Graham White (4.4): Anonymous Referee 1 wrote:   1. Are the results of the article, as specified in the summary, of significant interest for researchers in our area?   No. The main objective of the paper is to propose a solution to the Frame Problem which satisfies certain properties, which are convincingly argued for. My only but serious concern is that existing solutions seem to satisfy all of the requirements and that the author fails to argue for merits of his approach in comparison. In particular Reiter's theory [1] of generating successor state axioms from simple effect axioms fits perfectly the author's desiderata. No, it doesn't. One of my criteria is that the data for the problem should be what I describe as local, or, as Sandewall puts it (in a passage which I cite in the article),   Consider applications where every scenario describes a number of separate but interconnected objects, different scenarios involve different configurations, and each action has its immediate effects on one or a few of the objects, but indirect effects on objects which are connected to the first ones, in some sense of the word `connected'. ... action laws should only specify the ``immediate'' or ``primary'' effects of the action, and logical inference should be used for tracing how some changes ``cause'' other changes across the structure of the configuration at hand. However, Reiter's account starts from a statement of what he and Pednault describe as "effect axioms" (p. 360 of Reiter's article), which give, for each action and each fluent, conditions under which that fluent positively or negatively affects the fluent. These conditions, because they talk about all fluent-action pairs rather than just the fluents which are immediately affected by the action, are not concerned with the immediate or primary effects of actions but all of them. Now Reiter's paper does not explicitly consider the ramification problem, and, if we do not have ramification, it is entirely reasonable to suppose that actions can be described by effect axioms: actions then have no effects but their immediate effects. And it is certainly true that, in the absence of ramification, Reiter's solution does satisfy my desiderata (or, at least, the ones that I give in Table 1, apart, of course, for the requirement that the effect axioms should be local, which has little content in the absence of ramification). But, I am talking about a case with ramification, so that Reiter's methods do not apply; if we allow the effect axioms to talk about all effects, instead of just the immediate ones, then there is essentially no distinction between immediate and non-immediate effects. Neither can we hope to derive the unrestricted effect axioms from the local ones using merely classical logic (this, of course, is the assumption in Reiter's article; the effect axioms are supposed to yield all of the effects, local or non-local, using classical deduction). Consider the following example:   I move a block to a place L (this is the immediate effect of the action; the location of the block is changed). If the block is in a wet place, it becomes wet. (This is the description of how effects propagate). Location L is wet in the initial state. We want, of course, to conclude that the block becomes wet. However, in order to do this, we have to conclude that location L is wet, not in the initial state, but in the successor state. And we cannot conclude this by classical logic alone; considerations of examples like this (electrical circuits are a fruitful source) shows that, if we have a chain of propagating effects, we must, in general, solve the frame problem for the propagating causes up to stage  i  before we can know whether to apply the rules for the propagation to stage  i+1 .   ... And yet this work, which is among today's most cited papers in the area of Reasoning About Actions And Change, the author does not even mention, let alone compare it to his own method. No, that's true, I don't, but I do cite Murray Shanahan's book Solving the Frame Problem, which does contain a very clear and accurate account, not only of Reiter's work, but also of the work of Pednault and others which led up to it. C3-1. Anonymous Referee 1 (13.4): Dear author, You wrote:   ... And yet this work, which is among today's most cited papers in the area of Reasoning About Actions And Change, the author does not even mention, let alone compare it to his own method.   No, that's true, I don't, but I do cite Murray Shanahan's book Solving the Frame Problem, which does contain a very clear and accurate account, not only of Reiter's work, but also of the work of Pednault and others which led up to it. If I am not mistaken then Shanahan's book is mentioned only in a footnote and only as a side remark, not for the purpose of referring to an extensive account of work related to your's.   My only but serious concern is that existing solutions seem to satisfy all of the requirements and that the author fails to argue for merits of his approach in comparison. In particular Reiter's theory [1] of generating successor state axioms from simple effect axioms fits perfectly the author's desiderata.   But, I am talking about a case with ramification, so that Reiter's methods do not apply; if we allow the effect axioms to talk about all But Reiter's approach has been extended to dealing with state constraints and ramifications [2,3]. Several other successful approaches to the Ramification Problem emerged during the past five years or so; I mention [4,5,6]. Repeating myself, I am missing convincing arguments why your approach is substantially different and superior in comparison. [2] F. Lin and R. Reiter, State constraints revisited, J. of Logic and Computation 4(5), 1995. [3] F. Lin, Embracing causality in specifying the indirect effects of actions, IJCAI 1995. [4] N. McCain and H. Turner, Causal theories of action and change, AAAI 1997. [5] M. Thielscher, Ramification and causality, AIJ 89, 1997. [6] M. Denecker etal, An inductive definition approach to ramifications, ETAI 3, 1999. C3-2. The Author (27.4): Here's my reply to the referee's remarks.   But, I am talking about a case with ramification, so that Reiter's methods do not apply; if we allow the effect axioms to talk about all   But Reiter's approach has been extended to dealing with state constraints and ramifications [2,3]. Several other successful approaches to the Ramification Problem emerged during the past five years or so; I mention [4,5,6]. Repeating myself, I am missing convincing arguments why your approach is substantially different and superior in comparison. [2] F. Lin and R. Reiter, State constraints revisited, J. of Logic and Computation 4(5), 1995. [3] F. Lin, Embracing causality in specifying the indirect effects of actions, IJCAI 1995. [4] N. McCain and H. Turner, Causal theories of action and change, AAAI 1997. [5] M. Thielscher, Ramification and causality, AIJ 89, 1997. [6] M. Denecker etal, An inductive definition approach to ramifications, ETAI 3, 1999. Let's start with what appears to be a misconception. The referee writes "state constraints and ramifications", as if the two were synonymous. They are not, and one of the articles he refers to (by Deneker et al.) explains why not ([6], pp. 3f.):   we consider causal laws to be representations of how changes propagate. As such, causal laws may be but do not need to be related to state constraints. Below is an example. Assume a network with many input signals which can be directly modified through actions, an arbitrary internal structure, and one or more output lines. A counter on one of these output lines counts the number of times the output voltage changes from 0 to 1. [rules follow] The indirect effects described by the above rules are in no way related to a state constraint: there is no relation between the contents of the counter and the current state of the network." So there are examples which formalisms based on state constraints cannot cope with: this rules out the referee's reference [2]. Of the other approaches, [3], [4] and [6] suffer from the limitation (which Deneker et al., in [6], admit to) that multiple changes of the same fluent at the same time cannot occur. One can give well motivated examples which exhibit this behaviour: consider, for example, a modification of Deneker et al.'s counter example in which the counter is now connected to two of the output lines, and in which the input action may cause changes in either or both of them. The propagation of the effects may well result in the occurence of intermediate states of the counter when one of the output lines has had its effect but not the other. Similarly, the electrical circuit example in Thielscher's [5] (p. 341, Fig. 5) has intermediate states of fluents (namely, the light bulb being on) which are caused during the ramification process but which do not persist into the final state. Deneker et al. do describe such examples as "not well defined", but they do not argue for this restriction. So my approach, which correctly handles examples such as those given above, is more general than all of the cited approaches apart from Thielscher's [5], which also handles these approaches correctly. And regardless of the success or failure of my own approach, what we have done so far is to eliminate all but one of these supposedly "successful approaches to the Ramification Problem" by referring to arguments and examples found in the other ones. This makes me a little suspicious of the rules of this refereeing game as it is played in the AI community. After all, if I say "The sky is blue" and the referee says "No, you're wrong, the sky is green", then I may at least want to verify that the sky is, in fact, blue, just to check. But if the referee says "you're wrong, the sky is green AND the sky is red", then what do I reply? And if the referee cites supposedly "succesful approaches to the ramification problem", and not all of them can be simultaneously succesful because the later ones argue against the earlier ones (so that either the earlier ones are wrong, or the arguments and examples in the later ones are wrong); well, what can be concluded from that, other than that there are papers in the literature which disagree with mine (no surprise) and also with each other (also no suprise). What I want to insist on is the argument of my paper, and particularly the argument in Section 2.4. What I argue there is this: that the standard approach to these problems is unduly sensitive to vocabulary, because we can make formalisations, which seem to be adequate, of the same problem in vocabularies which seem to be logically equivalent (because they are equivalent in first order logic), and we find that when we apply the circumscription procedure to them, that one is successful and the other is not. And we seem to have no way of selecting one vocabulary rather than the other, other than that one gives a successful circumscription and the other does not. So this circumscription procedure does not seem to be anything that we can apply to a problem that we do not know the answer to: regardless of how adequate our formalisation might seem to be, we always have to face the possibility that there might be another formalisation (equivalent in first order logic, but using a different vocabulary) which gave different results under circumscription. We seem to have no way of differentiating between good vocabularies and bad, other than by looking at the results. Almost all of the cited approaches are, at least prima facie, susceptible to this sort of problem; they all rely, to some extent, on a preferred vocabulary -- explicitly in [2] and [3], because we have fluent-based circumscription; implicitly in [4], because of the definition of interpretations there as sets of fluents, and in [6] because of the use of reification in the definition of the fluent calculus. My own approach is not: I refer, in the article, to the fact that "in [the technical report] we show that we have a good notion of interpretation for theories of this sort, and that, in our example, we can change from the [one vocabulary to the other] without breaking anything". (p. 12 of the article). Furthermore, I have a semantics for my logic (also in the technical report); all of the above I am willing to expound at greater length if required (though I am still somewhat attached to the principle of separating the more philosophical and expository arguments from the mathematical details, and that was what I had hoped to accomplish in the separation between article and technical report). One could, finally, talk about the great computational advantages of approaches based on linear logic when compared to those based on circumscription or other of the conventional non-monotonic logics. So, finally, if you want a summary of what I think the advantages of my approach are, they would be: Correctness on a wider range of examples than any other approach, apart from Thielscher's [6]; Extensionality: that is, the formalism admits a robust notion of change of vocabulary (what is technically known as interpretation), and this notion of interpretation is supported by a semantics; Computational efficiency. C3-3. Murray Shanahan (28.4): Here's a small contribution to the Graham White paper debate. First, let me point out that I haven't (I'm ashamed to say) got around to reading Graham's paper, yet. So I'm not in a position to have any overall opinion on its merits. But I have followed the debate, and this has led me to the following thought. Graham lists the following advantages of his approach.   Correctness on a wider range of examples than any other approach, apart from Thielscher's [6]; Extensionality: that is, the formalism admits a robust notion of change of vocabulary (what is technically known as interpretation), and this notion of interpretation is supported by a semantics; Computational efficiency. Certainly (i) on its own, if true, suggests that the significance of the paper's contribution is sufficient for a journal. (I can't comment with respect to the other usual criteria for acceptance, not having read the paper.) But I think Graham is selling himself short. Merely to match the capabilities of existing formalisms using a radically different logic, namely linear logic, is itself a worthwhile contribution, assuming it's a non-trivial exercise. Redoing existing work in a very new way adds to our knowledge of the space of possible action formalisms, and could lead in all sorts of new directions. (Of course, the new way of doing things has to be radically different to be justified. Otherwise we end up with a proliferation of uninteresting variations on the same old theme.) Murray Q4. Anonymous Referee 2 (27.3): My recommendation as regards the acceptance of this paper for ETAI is no. Accordingly, I have perhaps to explain that. Roughly speaking, my answer is no, because there is a very little difference between the submitted and revised versions of the paper. On the other hand, the remarks, especially those made by Andreas Herzig, were quite important, and so they should be seriously taken into account in the final version. I am not going to be very detailed, but one example should illustrate this. Andreas writes:   I guess this relates to my main criticism: in order to identify actions in proofs, you must group together sequences of rules related to the same action. Answer of Graham:   No, not necessarily; if you look at the examples in `Actions, Ramification and Linear Modalities', you can see that you don't need to group rule applications together like this. The problem is that I would like to know certain important things not necessarily studying various tech reports, even if they are achievable by Internet. In preparing conference papers, we are usually short of space. But this is a journal paper and there is no reason to make it shorter than necessary. What is worse, many points mentioned in the open discussion have been completely ignored in the final version. I do not claim that the author cannot do certain things mentioned in the open disscussion phase. But his task is to convince me that he can. Since I am not convinced, my answer as regards the acceptance of the paper is no. A4. Graham White (4.4): Anonymous Referee 2 wrote:   My recommendation as regards the acceptance of this paper for ETAI is no. Accordingly, I have perhaps to explain that. Roughly speaking, my answer is no, because there is a very little difference between the submitted and revised versions of the paper. On the other hand, the remarks, especially those made by Andreas Herzig, were quite important, and so they should be seriously taken into account in the final version. I am not going to be very detailed, but one example should illustrate this. Andreas writes:   I guess this relates to my main criticism: in order to identify actions in proofs, you must group together sequences of rules related to the same action.   Answer of Graham:   No, not necessarily; if you look at the examples in `Actions, Ramification and Linear Modalities', you can see that you don't need to group rule applications together like this. Yes, in retrospect I agree that that was a little short. Here's a fuller account of my strategy with this. I give (on p. 10 of my article or so) a logical system which is an extension of linear logic by a modal operator  poss ; the important rule for  poss  is \Gamma |- A, \Delta -------------------- (*) \Gamma |- \poss A', \Delta where  A'  is obtained from  A  by a ramification transition. We must, however, add new rules to the system in order to be able to prove cut elimination: in particular, we must add the rule \Gamma, A' |- \poss B, \Delta ------------------------------ (**) \Gamma, A |- \poss B, \Delta where, again,  A'  is derived from  A  by a ramification transition. We then prove, as I have said, cut elimination for this system; as with most such proofs, the proof of cut elimination proceeds by rather elementary stages but is extremely long-winded (28 subcases or so). Now we can consider our representation of ramification and actions. We first describe our actions by their primary effects, namely by linear logic formulae of the form      a'lollipopa''    where  a'  and  a''  roughly correspond to Strips-like "delete lists" and "add lists", respectively. (They do not exactly correspond, because in order to be able to perform this action, the fluents in  a'  must be part of the initial situation, whereas the Strips delete list is only a list of the propositions which will be deleted if they are present.) Call an action, described like this,  alpha . Suppose also that we have a modality,  poss , which represents our ramification transitions. Now we can use the cut elimination theorem to show that the only valid proofs of a sequent of the form      A, alpha  |-  possB    correspond to the following sequences of rule applications: i) Applications of (**) to  A , yielding a state  a' × A'  (I represent the linear tensor product as *); ii) Applications of the rules for * and  lollipop , yielding a sequent      a'' × A'  |-  possB    iii) Applications of either (*) or (**), corresponding in either case to a ramification transition from  a'' × A'  to  B . iv) The identity axiom on either  a'' × A'  or  B , depending which rules we have applied. One can also prove that, in many cases, one can apply the rules in any order one likes; one can formalise this in so-called permutability theorems, saying that the applications of certain rules can be permuted around each other. In the case of the rules applied in this proof, we are free to permute rule applications except for the obvious restriction, namely that if  A  does not actually contain the "delete list"  a'  of the action, then (**) must be applied before we apply the rule for  lollipop . However, the proof-theoretic restrictions here correspond to our intuitive picture of what it is to perform an action in the presence of ramification: that is, the initial situation may first undergo a sequence of ramification transitions, then the action should accomplish its effects, and finally there should be a sequence of ramification transitions leading to the final situation. And in the "standard case", as it were, of the ramification scenario, we start with a situation  A  which is already stable under ramification transitions, so no initial applications of (**) are possible; we have no choice but to apply the rules for * and  lollipop  first. So, in order to represent action in this system, we do not have to impose any artificial grouping of rules: the proof theory gives us only the proofs that correspond to realistic sequences of action and ramification. Q5. Area Editor (29.3): Before I draw the conclusions from these two referee's reports, first some observations on procedure, and in particular on the room for debate in the context of referee's reports. Referee reports may fall into three categories: content, criteria, and policy, where criteria commentary consists of questions to our standard questions to referees; content commentary concern the material in the article as such, and policy comments concern or touch on the meta level as to what requirements we ought to have for ETAI accepted articles. In the simplest case, the referees only return comment according to the criteria, and in this case the area editor has no reason to add anything. Comments on content are treated as part of the open review discussion, and may be responded to by the author(s) and by others in the usual way. Comments on procedure, finally, will be interpreted in the context of what has been stated by the ETAI policy committee and the area editorial committee for our area. As area editor I may relate referee's policy comments to our established policy. If it is not clear about the issue under consideration, then the question will be referred to either of the mentioned committees, for their decision. However the readership is welcome to contribute to the meta level discussion as well: the ETAI is still formative, and comments by readers will be very useful for the policy and editorial committees in their consideration. In the present case, Anonymous Referee 1 returned criteria comments, but jers answer to question 1 also goes into questions of content. I will therefore give the author and others an opportunity to respond before the decision is made. Anonymous Referee 2 refers to the lack of consideration of issues that have been brought up by Andreas Herzig in the review discussion; please note by the way that referee 2 is not identical to Andeas and does not work with him. The referee refers to the fact that the article relies on a technical report, and suggests that it ought to be self-contained instead. In fact, the ease of access to articles over the Internet has raised the question whether we ought to relax the habit that articles be self-contained, and instead encourage inclusion of material by explicit linking. This was up for debate a year ago, and the answer was inconclusive: different readers have different preferences. The invitation for reference articles in our ETAI area represents one distinct step in the direction of reducing self-containment. That case is a bit different however: reference articles are supposed to be logically included in their entirety, whereas the present author refers to an unspecified but local position in a long technical report. In the present case we agree with Referee 2 that Herzig's questions would have motivated a more extensive coverage in the article itself, in particular because of the length of the referenced technical report. The broader policy issue of self-containedness in articles will be referred to the policy committee and our area editorial committee. We will be back with the decision about the article after the author has had an opportunity to respond. Q6. Area Editor (28.4): The outcome of this refereeing process is inconclusive. By the conventional wisdom, journal reviewing is supposed to identify which papers are to receive the quality stamp of approval, and which are not. This works fine if the quality of an article can in fact be identified by the review reports. But what do we do if there is a considerable remaining uncertainty - not that the paper is "medium good", but at the end of refereeing we still do not know what is the case -- we do not have the basis for a reliable verdict? The present article is apparently such a case. Both the two anonymous referees were strongly critical of the article. The author has answered to their criticism, and defended his case well, but some questions do remain. A first and obvious question is - if the proposed approach (as is claimed) is superior to all previously published approaches except one which it does not surpass, should it then be accepted to the journal? Many may be tempted to say no, but then quite a number of articles in the literature of this field ought not to have been accepted, so precedent is not consistent with such an abstract principle. Murray Shanahan, in his statement today, argues that it is in fact worthwhile to publish more than one approach in such cases. This is in itself an important methodological question in our area, where some continued exchange of opinions may be useful. From the point of view of the editorial decision, the debate has answered some questions but raised some new ones. In particular, consider the author's argument in his concluding remark that his approach has also two other advantages, besides epxressiveness, namely its extensionality and its computational efficiency. The problem is that neither of these advantages is very much substantiated in the article. With respect to extensionality, it would be necessary to show the advantage in concrete comparison with the most natural alternatives. The article makes an argument about problems in alternative approaches due to intensionality, but the problems he describes can possibly be explained as due to the use of domain constraints in the examples he refers to. One would have liked to see an argument why Thielscher's approach (which is otherwise mentioned as the contender) does not have the proposed extensionality property. Similarly, the author makes a general argument that "there is a well-developed technology for implementing proof search in these systems", but again a more concrete comparison with implementations of the major alternative approach(es) would be needed in order to defend this argument. These are objections to the effect that the article's arguments are incomplete, and not necessarily wrong. Some of these questions might be resolved by continued debate, but we also need to get to a decision with respect to the journal acceptance. The discussion can continue anyway, regardless of whether the article is accepted or not. And finally we must observe that the use of linear logic in itself often arouses strong feelings in the community, so it may not be possible to arrive at a consensus. With this we return to the original question: what is the most appropriate decision when the quality of an article is undetermined, with a high degree of uncertainty in the estimate? If a journal is seen as a means of active communication between researchers, which presumably is how modern journals started, then controversial contributions ought to be very highly valued. On the other hand, if journals are assigned prestige levels based on the perceived quality of their articles, and other articles in the same journal are assigned a quality level based on the journal's prestige, then it is in the interest of other authors that only uncontested articles be accepted. We may regret the contemporary practice of evaluating articles based on the ranking of journals, both because that practice institutionalizes lack of insight, and because of its side-effects on the editorial policies of the journals, but it is a fact of life and can not be ignored. Our solution to this dilemma uses the fact that we also publish the Electronic News Journal on Reasoning About Actions and Change, besides the ETAI. The primary purpose of the News Journal is to publish, on a monthly basis, the debate contributions and debate notes that appeared in the Newsletters, so that they also obtain formal, published status and can be cited. In any case, it seems appropriate that Graham White's article ought to be accompanied by the discussion that we have had here. In that way, it becomes transparent that the article is taken seriously by the community, but that there are strong differences of opinion about the proposed approach, and it is left to each reader to consider the arguments pro and con, and to make her or his own assessment. The conclusion, therefore, is to decline the submitted article for the ETAI, but to offer the author that the article be published in the ENRAC (News Journal) for April, 1999 together with the discussion and the present concluding comment. The continued discussion will then appear in later issues of the News Journal, like for all other articles.   Background: Review Protocol Pages and the ETAI This Review Protocol Page (RPP) is a part of the webpage structure for the Electronic Transactions on Artificial Intelligence, or ETAI. The ETAI is an electronic journal that uses the Internet medium not merely for distributing the articles, but also for a novel, two-stage review procedure. The first review phase is open and allows the peer community to ask questions to the author and to create a discussion about the contribution. The second phase - called refereeing in the ETAI - is like conventional journal refereeing except that the major part of the required feedback is supposed to have occurred already in the first, review phase. The referees make a recommendation whether the article is to be accepted or declined, as usual. The article and the discussion remain on-line regardless of whether the article was accepted or not. Additional questions and discussion after the acceptance decision are welcomed. The Review Protocol Page is used as a working structure for the entire reviewing process. During the first (review) phase it accumulates the successive debate contributions. If the referees make specific comments about the article in the refereeing phase, then those comments are posted on the RPP as well, but without indicating the identity of the referee. (In many cases the referees may return simply an " accept" or " decline" recommendation, namely if sufficient feedback has been obtained already in the review phase).