Re: BLD: two issues with the BNF

On Fri, 11 Jul 2008 18:37:41 +0200
Jos de Bruijn <debruijn@inf.unibz.it> wrote:

> 
> 
> Michael Kifer wrote:
> > On Fri, 11 Jul 2008 09:29:54 +0200
> > Jos de Bruijn <debruijn@inf.unibz.it> wrote:
> > 
> >>>> The second issue is not an error, but it can be considered misleading 
> >>>> (the BNF is too liberal): in the presentation syntax, rules are 
> >>>> quantified rule implications.  So, an atomic formula is not a rule and 
> >>>> may thus not be directly included in a group.  According to the BNF, an 
> >>>> atomic formula can be considered a rule; this is misleading.
> >>> There was a mistake in the math syntax. Groups should also allow atomic
> >>> formulas. Fixed.
> >> One more thing: atomic formulas can also contain variables.  I guess 
> >> that such non-ground atomic formulas should not be allowed in groups?
> > 
> > I see no reasons why such formulas should be disallowed. They are allowed as part of the KB, so why disallow them in groups?
> 
> 
> I thought all variables in BLD need to be explicitly quantified?


Oh, I see. Then probably those nonground atoms must also be quantified.
This will likely involve changes in the EBNF. I'll check what's the best way.

Received on Friday, 11 July 2008 16:44:05 UTC