Today

Today we announce the acceptance, after proper refereeing, of the paper by Marc Denecker, Daniele Theseider Dupré, and Kristof Van Belleghem: An Inductive Definition Approach to Ramifications.

Ernest Davis has prepared a "Guide to Axiomatizing Domains in First-Order Logics" which we publish as an ENRAC note, and where comments and discussion are most welcome.

The open discussions about our five reference articles have been concluded. Four of them are being refereed; for the fifth one the authors have indicated that they wish to make some minor changes.

Enrico Giunchiglia and Vladimir Lifschitz have written a paper that builds on the reference articles in relating several of the proposed approaches to each other. This is very much in the spirit of the intentions with our reference article initiative. The Giunchiglia and Lifschitz paper is entitled "Action Languages, Temporal Action Logics and the Situation Calculus"; its abstract and URL are found in this Newsletter.

The ETAI and its divisions now have a URL under .org, called etaij, so the entry webpage for reasoning about actions and change is found at http://www.etaij.org/rac/, and the entry webpage for ETAI as a whole is at is found at http://www.etaij.org/. Please update your links accordingly. Please change any links to the ETAI that you may have posted. (The old URL will remain valid for the immediate future, however).

The 'J' can be interpreted as 'Journal' or 'Junction', making a virtue out of necessity since "etai.org" had already been taken.

The ETAI represents a new approach to communicating research results as well as to communicating about research results, as we all know. There has been a lot of interest in this initiative recently, as witnessed by the article in the January, 21 issue of Nature. Under the headline "The writing is on the web for science journals in print", Declan Butler writes about new trends in research publishing; he mentions the ETAI and also refers to the possible adoption of a similar approach by the British Journal of Medicine.

The present area editor has also been invited to a number of workshops about publishing, including the AAAS/UNESCO/ICSU Workshop on Developing Practices and Standards for Electronic Publishing in Science that took place in Paris on 12-14 October 1998. I have as well received a number of inquiries from collegues in other fields who are interested in adopting the same approach as we are using.

Several of these articles and workshops are available on the net. In order to keep such information organized, we have introduced an additional part in the ETAI webpage structure, with the heading "Methodology and Publication in Research". This area will contain the same kinds of information services as we have for the ENRAC, except of course that it does not receive research articles for reviewing. If there is enough interest we may start a newsletter for that area, but at present it merely contains links to articles about electronic publishing in the ETAI and elsewhere.

To access the area for Methodology and Publication in Research (MPR), please proceed as follows: In the main webpage for the ETAI Junction, http://www.etaij.org/, select "ETAIJ information areas" in the lower part of the left-side menue. This will replace the blue menue with a similar one containing the link to MPR.

ETAI Publications

Additional debate contributions have been received for the following article(s). Please click the title of the article to link to the interaction page, containing both new and old contributions to the discussion.

Marc Denecker, Daniele Theseider Dupré, and Kristof Van Belleghem
An Inductive Definition Approach to Ramifications
   Review protocol: [in this pane]; with links: [frame] [noframe]

Articles

It's worthwhile to take a look at the article "Action Languages, Temporal Action Logics and the Situation Calculus", by Enrico Giunchiglia and Vladimir Lifschitz, which can be found at www.cs.utexas.edu/users/vl/mypapers/altalsc.ps. This paper relates major current approaches to actions and change, and builds on reference articles that were submitted to the ETAI in the autumn.

This use of the reference articles is of course very much in the spirit of the intentions with our reference article initiative. Here is the abstract of the article by Giunchiglia and Lifschitz:

Abstract. In the first part of the paper, we investigate the relationship between the action description language  C  and the situation calculus. Action description languages are based on the model of time that includes only two time instants: 0 for the beginning of the execution of an action and 1 for the end. The ontology of time in the situation calculus is much more elaborate. We show how to bridge the gap between these two ontologies by defining a translation from  C  into the situation calculus. The second part of the paper relates  C  to the formalism of temporal action logics (TAL) by showing how a fragment of  C  can be embedded into TAL.

Last year this Newsletter contained a discussion about ontologies for reasoning about actions. Giunchiglia and Lifschitz's article may represent a step towards a more analytical approach to comparing the existing approaches.

Methodology

Ernest Davis has sent us the following guide to the use of first-order logic for formalizing common-sense domains. The guide was written for students that study Knowledge Representation, and it should also be of interest for the ENRAC readership. Comments are welcome and will be organized like other ENRAC discussions.

1. Define a model or microworld, as specifically and precisely as the nature of the domain allows. (Obviously, a much more concrete model can be given in the domain of spatial relations than in the domain of human emotions.) You can then check for the soundness and consistency of your axioms by establishing that they are all true in the model.

   Do not cheat on your model. That is, if you find that you want to include in your axioms some new feature that is not in your model, do not just write down a new axiom. Rather, you should rethink the model to include the new feature, and check that all of your axioms still make sense relative to the revised model.

2. Make two tables enumerating all the sorts and all the non-logical primitives you use in your logic, with their definitions in terms of the model. If it is not possible to give necessary and sufficient conditions for the primitive, write down in English as precise a definition as you can manage, and try at least to bound the concept by giving some necessary conditions and some sufficient conditions.

3. If you want to adopt any notational conventions beyond a simple sorted FOL with equality, write them down explicitly (in English). E.g. if you want to posit the unique names property for constant symbols, write it down. If you have some standard convention for distinguishing fluents from related actions, write it down.

4. Some of the tenets of good programming style hold for axiomatizations as well:
   1. Non-logical primitives, like programming language identifiers, should be long enough that the reader can immediately know what they mean, but not so long that your axioms must be split up over many lines.
   2. Modularize. If you find the same subformula coming up again and again, define a new primitive to capture it.
   3. Use indentation and brackets to make the structure of the axiom apparent.

5. Cast a cold eye on every material implication. Keep in mind that  p ·-> q  means exactly  ¬ p v q , and nothing more.

6. If you have written   A(X)p(X) _^ q(X)  it is likely that you have made a mistake. Rewrite it as the two axioms   A(X)p(X)  and   A(X)q(X)  and see if it still makes sense.

7. If you have written   E(X)(p(X) ·-> q(X))  then it is 100 to 1 that you have made a mistake. Rewrite it in the logically equivalent form  ( E(X)¬ p(X)) v ( E(X)q(X))  and you will probably realize where you have gone wrong.

   The only exception to this I have ever seen is where the variable  X  does not actually appear in the left hand side of the implication; for instance, in a form like   A(Y) E(X)p(Y) ·-> q(X, Y) . Rewrite this for clarity as   A(Y)p(Y) ·->  E(X)q(X, Y) .

8. If you have the implication  p ·-> q , see if you can turn it into a biconditional  p <-> q . You may have to strengthen the right hand side to  p <-> (q _^ r) . This can be an easy way to get a more powerful theory.

   This does, however, require some care in choosing a grouping. Forms that are logically equivalent as implications may cease to be so when the implication is turned into a biconditional, and you have to choose the correct form. For instance, the two formulas

   A(X)( E(Y)X = Y+Y) ·-> even(X)

   and

   A(X, Y)X = Y+Y ·-> even(X)

   are equivalent. However, though the first can be turned into the correct biconditional

   A(X)( E(Y)X = Y+Y) <-> even(X)

   the second cannot.

   Another example: The assertion "If a triangle is equilateral then it is equiangular" can be represented

   	A(X)(triangle(X) ^ equilateral(X)) ·->
   	equiangluar(X)

   To turn this into a biconditional, however, requires separating out the condition  triangle(X)  as a condition on the entire biconditional.

   A(X)triangle(X) ·->       (equilateral(X) <-> equiangular(X))

9. Equality and function symbols are powerful representational tools; by all means, use them. However, there are a number of common errors to be avoided.
   1. The formula  X = Y  means that X and Y are identical things; it is not a translation of X is Y. I recently read a paper that contained the formulas,  Block1 = Red ;  Block2 = Blue ;  Block3 = Red . This would imply that  Block1 = Block3 .

   2. Keep in mind that functions in FOL are necessarily total. Therefore formulas like   E(Y)Y = f(X)  are always true and therefore vacuous.

   3. If you write down an FOL sentence containing the form  X = t  for some variable  X  and term  t , then you should think whether it is possible to simplify the sentence. In particular, the sentence   A(X)X = t ·-> p(X)  is equivalent to   A(X)p(t) . If  t  does not contain  X , then this is equivalent to  p(t) . Similarly,   E(X)X = t _^ p(X)  is equivalent to   E(X)p(t) . If  t  does not contain  X , this is equivalent to  p(t) .

      For example, if you are translating the sentence, "Your father is older than you are," (in the sense of "you" meaning "everyone"), it is natural to gloss this as "If  X  is the father of  Y  then  X  is older than  Y " and then to write it as

      A(X, Y)X = father(Y) ·-> older(X, Y)

      This can be expressed more elegantly as   A(Y)older(father(Y), Y) .

      On the other hand, the original form with the explicit implication may lend itself to conversion to a biconditional, as discussed in (8) above. For instance, the fact, "2 is an even prime," if expressed in the form   A(X)X = 2 ·-> (even(X) _^ prime(X)) , can be easily converted to the biconditional "2 is the only even prime,"   A(X)X = 2 <-> (even(X) _^ prime(X)) .

10. Keep in mind that FOL does not have negation as failure. This is not Prolog. This is particularly important in recursive definitions. If you try to define "above" as the transitive closure of "on" in the Prolog style

    	A(X, Y)on(Z, Y) ·-> above(X, X)
    	A(X, Y, Z)(on(X, Y) ^ above(Y, Z)) ·-> above(X, Z)

    you will be able to prove that some things are above others, but you will never be able to prove that something is not above something else, because this definition is consistent with everything in the world being above everything.

11. Don't do programming. FOL theories describe what's true, not how to compute things. If you find yourself yearning for loops, reassignable variables, data structures, or gotos, then either you're on the wrong track or you should stop working in FOL and switch to a programming language.

12. Check to see whether there exists a simpler or more general model for your axiomatization than the microworld you have in mind. For example, if you think a microworld involves gravity, then imagine a gravity-less version, and ask whether your axioms are still true in that. Another example: some theories of spatial regions in the AI literature are in fact true of arbitrary sets.

    Finding such an alternative model can have its pros and cons. Clearly, it means that you have not captured all aspects of your microworld. On the other hand, in a given application, you may not need these aspects. Identifying the axiomatization as a description of a simpler model may lead you to effective algorithms, decidability results, and so on. But, one way or another, it is definitely a fact worth knowing about an axiomatic system.

13. "Seek simplicity and distrust it." --- Alfred North Whitehead

Acknowledgements: Thanks to Pat Hayes, Hector Levesque, Vladimir Lifschitz, Rob Miller, and Ray Reiter for helpful criticisms and suggestions. The writing of this note was supported in part by NSF grant #IRI-9625859.