[Top] [All Lists]

Re: [ontolog-forum] Yet another ontology definition

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Alex Shkotin <alex.shkotin@xxxxxxxxx>
Date: Wed, 30 Jun 2010 22:40:20 +0400
Message-id: <AANLkTikJ3OXVzxCOQIptY1LeFc3l-05rZPMjYf8F_Lx1@xxxxxxxxxxxxxx>
>I assume that your sample axiom that begins "harzburgite(x) = "
>has an implicit universal quantifier.


I was wrong to use "=" instead of "is an abbreviation for" in definition statement.

I hope this is better:

Definition. harzburgite(x) is an abbreviation for:

not (pyroclastic(x) or kimberlite(x) or lamproite(x) or lamprophyre(x) or charnockite(x))

and plutonic(x)

and VPC_carbonates(x)≤50 and VPC_melilite(x)≤10 and VPC_kalsilite(x)=0


We use usual math style to keep definitions separately and need not "possible definition" axiom (at this stage):

∀x harzburgite(x) not (pyroclastic(x) or kimberlite(x) or lamproite(x) or lamprophyre(x) or charnockite(x))...

as we use usual substitution technique to prove theorems manually.

For ex. we have definition for dunite (you can imagine;-), and a theorem:

∀x not(harzburgite(x) and dunit(x))

After substitution of definitions it may be restructured to tautology.

But we do need "possible definition" axiom when we move to OWL 2 with linear equations extension.

For us definition keeps answer to the question - "What does it mean to be a harzburgite?"
- Well, any igneouse rock that is not pyroclastic and not kimberlite...

Thank you,


John Sowa

Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (01)

<Prev in Thread] Current Thread [Next in Thread>