Re: Rules WG -- draft charter

I have a number of comments on the draft rules WG charter, revision 1.26.

I worry about the tieing together of rules and justifications.
Justifications can be quite difficult to deal with, except under certain
circumstances, even if limited to rule systems.  In particular, checking
whether the application of a non-monotonic rule is justified can be
intractable or even undecidable.

I also worry about the condition that justifications are only to be used to
justify how rules were used to reach a conclusion.  Even in an RDFS plus
rules setting, there is more going on than just rule activity.  If this is
the case, how will the RDFS inferences be recorded?  The situation is much
more complex in an OWL plus rule setting.

The document appears to me to be internally inconsistent, particularly with
respect to jusifications.  In Section 1 it states that justifications are
to be used to ``allow the expression of of the knowledge of how certain
rules were used to reach conclusion''.  In Section 2.1 it states that the
working group is supposed to address ``a language for the exchange of
proofs'', which is a much more ambitious scope than recording rule traces.

The document appears to require that rules be equivalent to material
implications, which is not their treatment in many rule systems.  In
particular, in some rule formulations that allow disjunctive information
rules with false consequents are not equivalent to classical negation.

The document again brings up the desire to put everything in RDF, both
syntactically and semantically.  The Web Ontology Working Group spent a lot
of time wrestling with a similar mandate before ultimately settling on a
partial solution that only works because of several characteristics of OWL,
which would not be shared by a rules language.  I forsee that a similar
mandate for rules would end up causing a similar delay for the rules
working group.

It is not the case that proof checking is ``computationally much easier
than theorem proving''.  In decidable logics the length of a proof may
be similar to the number of computational steps required to proove a
particular result.  This may lead to a PSPACE deduction procedure but proof
checking requiring exponential space just to store the proof.

Peter F. Patel-Schneider
Bell Labs Research

Received on Monday, 10 November 2003 10:45:46 UTC