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

>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