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.

Hi Victor,

In the "old" Part 7 I tried just that, a full OWL representation of what is now called the "lifted template" (in those days the "longhand template".
This was shot to flames and the FOL code came instead.
One point of attention is how you identify the "hidden" objects and its (rdf)properties, i.e. the ones that are not in the signature.

Hans,

FOL is good for human understanding and clear for mathematicians. I prefer FOL, but I see that my computer and my software engineers are not satisfied.

As far as I understand, in OWL we define the template as a class of n-tuples by placing various restriction on its members, and restrictions themselves are formulated as class membership rules. I hope there are no principal difficulties in forming restrictions with some unnamed resources declared inside of definition - exactly what we do with skolemization in FOL.

Victor,

Why don't your computer and software engineers not tell what their preference would be?

I am neither, so my question may be very dumb: can't they produce something more useful starting with the FOL code?

Hans,

Software people are putting forward one specific requirements - unambiguous URI identification of templates in the axiom. As I've tried to explain, the solution have to come from logicians and/or OWL experts.

Solutions from software engineers are too often language/system dependant. That's exactly what we are doing now in our Editor - internal format suitable to keep info derived from FOL axioms, OWL definitions, IIP Pattern database and all future formats to appear.

In the time that Johan Kluewer wrote the basis of part 7, the rule language of choice was SWRL. He took FOL to be interdependent of computer languages. However he mentioned the move to RIF which was not developed back then.

Via this link http://standards.iso.org/ittf/licence.html you can download ISO/IEC 24707 - Information technology — Common Logic (CL): a framework for a family of logicbased languages, free of charge for personal use.

Two quotes:
5.1.1:
Common Logic syntax and semantics shall provide for the full range of first-order syntactic forms, with their
usual meanings. Any conventional first-order syntax will be directly translatable into Common Logic without
loss of information or alteration of meaning.

C.1:
XCL is an XML notation for Common Logic. It is the intended interchange language for communicating
Common Logic across a network. It is a straightforward mapping of the CL abstract syntax and semantics into
an XML form.

Does anybody have hands-on experience with CL?

The NIST tool is parsing the logic (from Onno's tool?) into Common Logic objects using the object definitions in the Ontology Definition Metamodel. ( http://syseng.nist.gov/cre/odm-tree ) -- click on org.omg.odm, and then CL.

I'm happy with a human-readable form (CLIF, the KIF like form) for use in the Part 8 XML. I don't know that we need an XML form.

I think Common Logic semantics would be appropriate.

I've had positive experiences with KIF and first order reasoners.