RE: Rules WG -- draft charter

At 19:34 -0500 11/11/03, Boley, Harold wrote:
>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

For what it is worth, I have been working on some proof checking 
stuff for a while now, doesn't really depend as much on the model 
theory as you might think because most proofs are a sequence of steps 
validated by a logic -- we assume the axioms are defined elsewhere 
and there is agreement.

Thus, given A and A -> B  one can write something like
   B  log:followsfrom (A->B, A ) log:using log:modusPonens
where the model theory is needed to be there to make sense of the 
"modus ponens" and the like, but does not need to compelte before one 
could start working on how to represent "Follows from" and "using" 
and the like.

  -JH


-- 
Professor James Hendler			  http://www.cs.umd.edu/users/hendler
Director, Semantic Web and Agent Technologies	  301-405-2696
Maryland Information and Network Dynamics Lab.	  301-405-6707 (Fax)
Univ of Maryland, College Park, MD 20742	  240-277-3388 (Cell)

Received on Tuesday, 11 November 2003 19:43:53 UTC