Re: [SWC] comments/review SWC - part2

On Mon, 30 Jun 2008 16:33:49 +0200
Jos de Bruijn <debruijn@inf.unibz.it> wrote:

> 
> >> My point was that the thing in the BLD presentation syntax is called 
> >> "document" and not "RIF-BLD-document" or "RIF document".
> > 
> > I see. Actually, it is called "document formula" or "RIF-BLD document formula".
> 
> You are right.  I forgot the "formula" part.
> 
> But, concerning "RIF-BLD document formula": it is used in some places 
> (even "RIF-BLD document" is used), but there is no definition.

I now added "RIF-BLD" in front of "document formula" in the definition.

> I would suggest to include this definition where "document formula" is 
> defined (i.e., section 2.4), or even add an additional section.
> on that note, when strictly reading the definitions, annotations do not 
> seem to be part of document formulas.  So, I would recommend to define 
> documents after defining annotations, and taking the annotations into 
> account in the definition.

I now added a definition of "RIF-BLD document" as a "RIF-BLD document formula"
with or without an annotation. This is in the short section about annotations.

> Actually, in order to allow annotations in front of arbitrary sub 
> formulas, annotations should be included in the definition of a formula. 
>   For example, one bullet in the Definition (Well-formed formula) could be:
> * ''Annotated formula'': If psi is a well-formed formula, then (* id phi 
> *) psi  also a well-formed formula.

I added a clarifying clause that annotations are allowed for subformulas and
subterms. However, I did not add annotated formulas among the bullets in the
main definition, since it would complicate things. This is because, I assume,
we do not want annotations to be added to already annotated terms and formulas.
So, the nice recursive nature of the definitions would have to be spoiled with
qualifications.


	--michael  


> Thus, Jos
> 
> > 
> > 
> > 	--michael  
>