- From: Kashyap, Vipul <VKASHYAP1@PARTNERS.ORG>
- Date: Mon, 5 Nov 2007 10:55:28 -0500
- To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
- Cc: <public-owl-wg@w3.org>, <dlm@ksl.stanford.edu>
>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.
Received on Monday, 5 November 2007 15:55:59 UTC