View unanswered posts | View active topics It is currently Wed Jan 22, 2020 1:30 am

Reply to topic  [ 8 posts ] 
 Template FOL axiom encoding 
Author Message

Joined: Mon Feb 27, 2012 11:01 pm
Posts: 282
Location: Moscow, Russia
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 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

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.

Fri Nov 16, 2012 9:57 pm
Profile WWW

Joined: Sun Jan 22, 2012 10:02 pm
Posts: 283
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.

Sat Nov 17, 2012 10:43 am

Joined: Mon Feb 27, 2012 11:01 pm
Posts: 282
Location: Moscow, Russia

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.

Sat Nov 17, 2012 12:02 pm
Profile WWW

Joined: Sun Jan 22, 2012 10:02 pm
Posts: 283

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?

Sat Nov 17, 2012 3:45 pm

Joined: Mon Feb 27, 2012 11:01 pm
Posts: 282
Location: Moscow, Russia

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.

Sun Nov 18, 2012 12:00 pm
Profile WWW

Joined: Sun Jan 22, 2012 9:14 pm
Posts: 189
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.

Mon Nov 19, 2012 3:09 pm

Joined: Sun Jan 22, 2012 10:02 pm
Posts: 283
Via this link 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:
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.

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?

Thu Nov 29, 2012 10:47 am

Joined: Mon May 07, 2012 1:20 pm
Posts: 10
The NIST tool is parsing the logic (from Onno's tool?) into Common Logic objects using the object definitions in the Ontology Definition Metamodel. ( ) -- 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.

Fri Feb 08, 2013 9:18 pm
Display posts from previous:  Sort by  
Reply to topic   [ 8 posts ] 

Who is online

Users browsing this forum: No registered users and 0 guests

You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot post attachments in this forum

Search for:
Jump to:  
eXTReMe Tracker
Powered by phpBB® Forum Software © phpBB Group
Designed by ST Software.