RE: Rules WG -- draft charter

Harold:
> 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"
> (http://www.cis.temple.edu/~ingargio/cis587/readings/tms.html)
> -- 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.

Right indeed, one can do better than the typical Yes/No output
of Prolog systems and this is so mechanically straightforward
while having such a high support potential.

> 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.

Well, maybe the test results could written in that proof language
(supposing there is a test subgroup) and then it will indeed be
a bit shifted in time, but not that much I guess :-)


--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Received on Wednesday, 12 November 2003 05:26:13 UTC