Template FOL axiom encoding
Posted: Fri Nov 16, 2012 9:57 pm
The need for a standard way to relate OWL template definition to its FOL axiom is universally recognised. The latest proposal can be found in http://15926.org/viewtopic.php?f=6&t=74 .
All attempts known to me are built around the same idea - use text representation of FOL axiom in the predicate notation of Part 7. This approach for me has two major problems - one for practical implementation, another rather theoretical.
1. From the implementation side the problem is that inside a FOL axiom templates are not referred by URIs. It is certainly not a problem for implementation if only base and proto templates from a standard predefined set are included in the axiom.
But imagine that I'm defining some company-level template CompositionOfThisAndThat with URI http://xyzco.com/templates#CompositionOfThisAndThat and I need to use another local template CompositionOfThis in its FOL axiom. How can I use its URI to show unambiguously that it is indeed http://xyzco.com/templates#CompositionOfThis?
2. From the theoretical point of view as far as I understand, OWL itself contains full set of FOL constructs used in template axiom construction. My understanding is rather vague, but I'll try to describe general idea and I hope it will tell something to OWL professionals here.
The template defined by its owl:Class description as n-ary relationship already contains part of the axiom - that part which defines role type restrictions. Probable it is possible to augment class definition with other types of restrictions required for full axiom - predicate restrictions formed by lower-level templates included in the axiom?
If full axiom encoding in OWL is possible - it'll solve the first problem also, as templates in OWL are referenced by URIs.
Hope this has some sense and can be criticized at least.
All attempts known to me are built around the same idea - use text representation of FOL axiom in the predicate notation of Part 7. This approach for me has two major problems - one for practical implementation, another rather theoretical.
1. From the implementation side the problem is that inside a FOL axiom templates are not referred by URIs. It is certainly not a problem for implementation if only base and proto templates from a standard predefined set are included in the axiom.
But imagine that I'm defining some company-level template CompositionOfThisAndThat with URI http://xyzco.com/templates#CompositionOfThisAndThat and I need to use another local template CompositionOfThis in its FOL axiom. How can I use its URI to show unambiguously that it is indeed http://xyzco.com/templates#CompositionOfThis?
2. From the theoretical point of view as far as I understand, OWL itself contains full set of FOL constructs used in template axiom construction. My understanding is rather vague, but I'll try to describe general idea and I hope it will tell something to OWL professionals here.
The template defined by its owl:Class description as n-ary relationship already contains part of the axiom - that part which defines role type restrictions. Probable it is possible to augment class definition with other types of restrictions required for full axiom - predicate restrictions formed by lower-level templates included in the axiom?
If full axiom encoding in OWL is possible - it'll solve the first problem also, as templates in OWL are referenced by URIs.
Hope this has some sense and can be criticized at least.