- From: Boley, Harold <Harold.Boley@nrc-cnrc.gc.ca>
- Date: Tue, 11 Nov 2003 19:34:26 -0500
- 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" (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. 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. Best, Harold
Received on Tuesday, 11 November 2003 19:34:32 UTC