Problem with RIF-Core specification [was Re: Urgent: Issue with RIF-Core EBNF Grammar?]

Axel, all,

I think there are a number of basic problems in the specification of RIF
Core formulas. In particular:

1- the notion of "rule conclusion" is never defined. In fact, neither the
notion "rule" nor "conclusion" is defined anywhere. This leads to several
ambiguities: e.g., is a variable-free rule implication a rule? perhaps. Is a
variable-free atomic formula a rule? there is no wording in BLD that would
suggest this.

2- if we were to assume that "rule" means "RIF-BLD rule", which is the
assumption I would naturally make from the BLD spec, then I read the
restriction
"Equality terms and class membership terms *cannot* occur in rule
conclusions -- they are allowed only in rule premises."

in [1] as saying that equality terms and class membership terms are not
allowing the the conclusions of RIF-BLD rules. Full-stop.
This means they are allowed in variable-free rule implications, universal
facts (although some text in BLD may suggest these are a kind of RIF-BLD
rules), and variable-free atomic formulas.
I am quite sure we decided not to allow the assertion of equality. I do not
recall exactly what we decided about facts concerning class membership
(i.e., a#b). Does anybody recall what we decided here?

In any case, this ambiguity needs to be resolved. Notice that the EBNF
grammar does not help us here, since it is non-normative.


Best, Jos

[1] http://www.w3.org/TR/2010/PR-rif-core-20100511/#Formulas_of_RIF-Core

On Tue, May 11, 2010 at 6:15 PM, Axel Polleres <axel.polleres@deri.org>wrote:

> Hi folks,
>
> We are working on a parser with some students and I am afraid my student
> found something awkward in the RIF Core grammar, see mail below.
>
> Indeed, I think he poked into a quite weird issue:
> It doesn't make sense to allow class membership terms in rule bodies, if
> they can't appear at all in *any* facts.
> The current grammar and the restrictions in Section 2.3 though only allows
> uniterms and frames as facts.
>
>
> To repair this
>
> 1) We'd need to change in Section 2.3 Formulas of RIF-Core:
>
>  * Equality terms and class membership terms cannot occur in rule
> conclusions -- they are allowed only in rule premises.
> -->
>  * Equality terms cannot occur in rule conclusions -- they are allowed only
> in rule premises.
>  * Class membership terms can only occur in rule premises or as ground
> facts.
>
> 2) a proposal to fix the grammar in Section 2.6 would  be:
>
> In the Rule Language grammar:
>
>  CLAUSE         ::= Implies | ATOMIC
>  -->
>  CLAUSE         ::= Implies | ATOMIC | GROUNDTERM '#' GROUNDTERM
>
>
>
> sorry for spotting this now only, but I am afraid this is severe.
> the fix is not very problematic, though.
>
> Axel
>
>
>
>
> Begin forwarded message:
>
> > From: "Obermeier, Philipp" <philipp.obermeier@deri.org>
> > Date: 11 May 2010 16:26:50 GMT+01:00
> > To: "Polleres, Axel" <axel.polleres@deri.org>
> > Cc: "Marco Marano" <marcomarano83@gmail.com>
> > Subject: RIF-Core: EBNF, equality/memberhip facts
> >
> > Hi Axel,
> >
> > I found a minor error in the EBNF grammar [1] for RIF-Core (Altough,
> > this grammar is informative due to the lack of well-formedness checks,
> > it is also defined as strict superset of RIF-Core.).  Within this
> > grammar you cannot derive Equality or Membership (ground) facts since
> > the ATOMIC rule's rhs is restricted to atomic formulas excluding
> > Equality/Membership formulas. Apparently, this restriction is well
> > justified since ATOMIC may appear in rule heads (cf. IMPLIES rule's
> > rhs), for which Core forbids Equality and Membership formulas. In
> > conclusion, an introduction of a new ATOMIC_FACTS grammar rule extending
> > ATOMIC by Membership/Equality  would solve this issue w/o breaking the
> > restriction for atoms in rule heads.
> >
> > Best
> > Philipp
> >
> > [1]
> >
> http://www.w3.org/2005/rules/wiki/Core#EBNF_Grammar_for_the_Presentation_Syntax_of_RIF-Core
> >
> > --
> > Philipp Obermeier
> > Digital Enterprise Research Institute, National University of Ireland,
> Galway
> > email: philipp.obermeier@deri.org
>
>


-- 
Jos de Bruijn
 Web:          http://www.debruijn.net/
 LinkedIn:     http://at.linkedin.com/in/josdebruijn