Re: ISSUE-52 (Explanations): Specification of OWL equivalences and rewriting rules for explaining inferences

Dear Vipul,

I have no idea who you are replying to. Please consider Peter's  
remarks about this in his 'quoting conventions' message.

Best,

	Rinke



On 5 nov 2007, at 16:55, Kashyap, Vipul wrote:

>
>
>> What tools would generate these (potentially very large) constructs?
>> What tools would consume them?
>
> [VK] These constructs would be generated by ontology reasoners.
> They would be consumed by: (a) other ontology reasoners;
> (b) different ontology development tools, e.g., P4, Swoop, etc.
> (c) any general ontology versioning, maintenance and consistency  
> checking
> application.
>
>> How are you going to account for variances between proof strategies
>> within a particular reasoning technology or variances between  
>> different
>> reasoning technologies?
>
> [VK] What I am proposing is a standardized approach to repreent
> - Proofs
> - Entailments
>
> The representation scheme I am proposing is independent of the  
> underlying
> technology (I presume you mean, Fact++ vs Pellet etc.). The  
> representation
> scheme would be dependent on OWL 1.1 constructs, though.
>
> This scheme would represent the proof output by a reasoner. Just as  
> we do not
> have constructs that specify the execution of the tableaux  
> algorithm, we would
> not specify the actual proof strategy used by a reasoner.
>
>> What are the characteristics of these constructs?  For example, I can
>> think of a whole spectrum of specifications of proofs, ranging from  
>> ones
>> where a proof could always be "The ontology just entails the  
>> answer" to
>> ones that have the effect of nailing down exactly how an OWL reasoner
>> must behave.
>
> [VK] These constructs would characterize the notion of an  
> entailment. Based on
> the example given to Alan, a rough specification could be:
>
> Proof => ListOf(Entailment)
> Entailment => Antecedent entails Consequent
> Antecedent => ListOf(Axiom)
> Consequent => ListOf(Axiom)
> Axiom => OWL 1.1 Axiom
>
> So, my proposal is to declaratively specify an entailment and  
> constructs for the
> same. How specific reasoners come up with this entailment is an  
> implementation
> detail as long as they "report" their proofs and explanations in the a
> standardized specification similar to the above. The analogous  
> argument here is
> that OWL 1.1 doesn't provide constructs that trace the execution of  
> the tableaux
> algorithm.
>
>> What evidence do you have that the "explanations" can be divorced  
>> from a
>> particular UI context, and thus suitable for transmittal between  
>> tools
>> at all?
>
> [VK] If we agree that OWL 1.1 can be divorced from a particular UI  
> context then,
> given that what I am proposing is a thin "wrapper" layer around OWL  
> 1.1, it
> should have the same properties. The new constructs proposed do not  
> destroy the
> UI independence property which OWL 1.1 has.
>
>> In general, WGs have to have one or more starting points - reasonably
>> well-worked out proposals that have a community already.  What is the
>> starting point here?  If there is none, then how can we proceed?
>
> [VK] One starting point could be Deborah's Proof Markup Language  
> Specification.
> That said, I think we can limit the scope in the context of the WG  
> to a very
> thin layer of proof specifications. Maybe as Jim suggested, we can  
> just "stuff
> them as strings" in annotation properties for now.
>
> But I do clearly see a value in saving and sharing these proofs  
> somehow!
>
> Hope that clarifies some of the questions you had. Look forward to  
> further
> feeback and suggestions.
>
> Regards,
>
> ---Vipul
>
>
> The information transmitted in this electronic communication is  
> intended only for the person or entity to whom it is addressed and  
> may contain confidential and/or privileged material. Any review,  
> retransmission, dissemination or other use of or taking of any  
> action in reliance upon this information by persons or entities  
> other than the intended recipient is prohibited. If you received  
> this information in error, please contact the Compliance HelpLine at  
> 800-856-1983 and properly dispose of this information.

----------------------------------------------
Drs. Rinke Hoekstra

Email: hoekstra@uva.nl   Skype:  rinkehoekstra
Phone: +31-20-5253499    Fax:   +31-20-5253495
Web:   http://www.leibnizcenter.nl/users/rinke

Leibniz Center for Law,         Faculty of Law
University of Amsterdam,           PO Box 1030
1000 BA  Amsterdam,            The Netherlands
----------------------------------------------

Received on Monday, 5 November 2007 16:12:44 UTC