From MathWeb

Problem statement: We can't express rules in (OWL-)DL. But we need them to express certain things about OMDoc. Maybe we should express them in SWRL or the upcoming RIF?

This discussion is partly obsolete, as things will improve with the upcoming OWL 1.1 (see this remark).

Note to Achim and Normen: We may not need rules in what you call document ontology, but in other parts of the formal foundations of OMDoc-based applications we do. --Clange 18:29, 3 April 2007 (CEST)

Contents 1 Desirable rules 1.1 Implicit imports of nested theories 1.2 Assertion depends on definition (OBSOLETE) 1.2.1 Discussion 1.2.2 Done 2 Ideas for usable reasoners 3 Where are the boundaries of DL? 3.1 What is possible?

Desirable rules

Let's collect rules that we'd like to have but that cannot be expressed in OWL-DL here. Please use a Prolog-like syntax. --Clange 16:52, 17 July 2006 (CEST)

Implicit imports of nested theories

imports(nested-theory, home-theory) :- homeTheory(nested-theory, home-theory).
imports(nested-theory, other-theory) :- homeTheory(nested-theory, ENCLOSING-THEORY), imports(ENCLOSING-THEORY, other-theory).

Assertion depends on definition (OBSOLETE)

depends(assertion, definition) :- uses(assertion, SYMBOL), defines(definition, SYMBOL).

uses is not yet implemented. It means that some symbol is used in a formula in an assertion, e.g. for OpenMath: omdoc:FMP/om:OMOBJ contains some OMS.

Discussion

A question on that: We could solve this in DL if we declared uses as a subproperty of dependsOn, which would IMHO make sense anyway. As regards the symbol and the definition, in which way does the dependency relation point? In OMDoc/XML, we have definition for="#symbol", but actually the symbol itself is re-used elsewhere, and its meaning depends on the definition! So we could assert that defines(def, sym) implies depends(sym, def) (notice the order!) and get depends(ass, def) for free by an OWL-DL reasoner, as the dependsOn relation is transitive. Can we do it this way? --Clange 17:49, 17 July 2006 (CEST)

Maybe it's of advantage to entirely invert the direction of the depends relation between a symbol and a definition. Maybe I've been misled by the "for" attribute, which seems to point from the definition to the symbol. --Christoph 19:28, 23 October 2006 (CEST)

Andreas Franke means: Do it this way, they did the same in MBase. (See mail "Re: [OMDoc-dev] System ontology: which direction has the dependency relation between a symbol and a definition?" posted to OMDoc-dev on 24 October 2006)

The MBase paper from 2000 distinguishes "primitive" symbols (no defition) from "defined" ones (one or more (then: equivalent!) definitions). --Christoph 20:57, 18 December 2006 (CET)

Your answer here, appropriately indented by ":", please sign your post.

Done

The current version of the ontology contains the relation Symbol-hasDefinition-Definition, which partly solves the problem described above. --Clange 16:53, 30 March 2007 (CEST)

Ideas for usable reasoners

• Hoolet (OWL-DL + SWRL)
• Jess (SWRL can be converted to that system; non-free)
• KAON2 (OWL-DL + DL-safe SWRL; non-free)
• KRHyper (first order logic; can OWL be imported?)
• see also:
  • lecture about rules and OWL (German)
  • N3Logic: proposal of a new semantic web logic calculus

Where are the boundaries of DL?

Is there a possibility to express rules by means of reified properties (i.e. properties modeled as classes) in OWL-DL? Consider the following example (abbreviated notation):

owl:Class "SomeGenericRelation"

owl:ObjectProperty "from"
 rdfs:domain SomeGenericRelation
 rdfs:range OMDocConcept

owl:ObjectProperty "to"
 rdfs:domain SomeGenericRelation
 rdfs:range OMDocConcept

owl:Class "TheoryImport"
 subClassOf SomeGenericRelation
 owl:restriction on from
  owl:allValuesFrom Theory
 owl:restriction on to
  owl:allValuesFrom Theory

Can we use these to push the boundaries of DL towards rules? --Clange 13:22, 20 July 2006 (CEST)

What is possible?

Here are some rules that OWL does understand:

impliedInstanceOf(thing, class) :- instanceOf(thing, class).
impliedInstanceOf(thing, class) :- instanceOf(thing, SUBCLASS), impliedSubClass(SUBCLASS, class).

impliedSubClass(sub, super) :- subClass(sub, super).
impliedSubClass(sub, super) :- subClass(sub, C), impliedSubClass(C, super).
% classes defined as unions of other classes
% BTW: Can you use universal quantifiers on the right side of a Prolog clause?
impliedSubClass(unionclass, super) :- "forall SUB: hasUnionMember(unionclass, SUB) => subClass(SUB, super)".

Can you think of more? --Clange 14:58, 20 July 2006 (CEST)

Reportedly, there are translators from OWL-DL to Prolog – but are they usable? Clange 15:25, 20 July 2006 (CEST)