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
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.