W3C home > Mailing lists > Public > www-rdf-rules@w3.org > November 2003

RE: Rules WG -- draft charter

From: Boley, Harold <Harold.Boley@nrc-cnrc.gc.ca>
Date: Tue, 11 Nov 2003 19:34:26 -0500
Message-ID: <10C94843061E094A98C02EB77CFC3287026DF691@nrcmrdex1d.imsb.nrc.ca>
To: 'Sandro Hawke' <sandro@w3.org>
Cc: "'www-rdf-rules@w3.org'" <www-rdf-rules@w3.org>

Hi Sandro,

>> The attached html contains most sections from your draft
>> with some change suggestions in red using DanB's CSS style.
> Thank you, good stuff.   You're pretty sure about "proof" instead of
> "justification"?   I'm getting conflicting input on that.   Does "proof"
> help tell the people who want it excluded that it's really only the
> simple stuff?  (the record of rules used)

Yes, the technical term "proof" is less loaded than "justification".
For example, it does not have the connotations stemming from
Justification-based Truth Maintenance System (JTMS) research.
Giorgio Ingargiola's (http://www.cis.temple.edu/~ingargio/)
article on "Problem Solving and Truth Maintenance Systems"
-- while interesting -- would thus not be on topic for this WG.

Yes, a "proof" can simply be a representation of the rules and
facts used to reach a conclusion, taking into account possible
variable bindings (the 'substitution'). This representation may
just chain some rules sequentially and end in a fact. It may also
employ certain rules as a "proof tree" with facts at all the leaves.
Since we need to come up with an (RDF, XML, ASCII) representation
of rules and facts anyway, and since the substitution could, e.g.,
be implicitly represented via specialized rules and facts, such a
simple proof language should be achievable as a WG subpackage.

Because this proof language would be dependent on the rule language,
it would be necessary to start this subpackage only ca. 6 months
after the rule language subpackages themselves. One of these earlier
subpackages would then also need to go beyond the model theoretic
semantics of the rule language. Clearly, only after a proof theoretic
('operational') semantics is fixed, does it make sense to work on
a language for representing proofs according to that proof theory.
Since several proof theories can 'implement' the same model theory,
fixing one of them -- while chosen carefully to fit Semantic Web and
Web-of-Trust needs -- would only have an exemplary character.

Received on Tuesday, 11 November 2003 19:34:32 UTC

This archive was generated by hypermail 2.3.1 : Wednesday, 2 March 2016 11:10:14 UTC