Re: [protege-user] Enumerated Classes and Puns: TBox or ABox?

All OWL2 Primer <https://www.w3.org/TR/owl2-primer/> is about People. And I
think you use punning
<https://www.w3.org/TR/owl2-primer/#OWL_2_DL_and_OWL_2_Full> as there.

Using classification I mentioned EquivalentClasses is from Table 5 [1] and
comes to Tbox.

Maybe the best way is to say that you split ontology into a theoretical
part (Theory box) and a particular structure part (Data box).

Alex

[1] OWL 2 Functional Style operators from HOL point of view
<https://www.researchgate.net/publication/336363623_OWL_2_Functional_Style_operators_from_HOL_point_of_view>
(4)Table 5. Satisfaction of Class Expression Axioms in an Interpretation

Axiom

and HOL-definition header

Condition

HOL-definition body

SubClassOf( CE1 CE2 )

(CE1)C ⊆ (CE2)C

∀z:o CE1(z) → CE2(z)

EquivalentClasses( CE1 ... CEn )

(CEj)C = (CEk)C for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n

⋀1≤j≤n⋀1≤k≤n ∀z:o CEj(z) ≡ CEk(z)

DisjointClasses( CE1 ... CEn )

(CEj)C ∩ (CEk)C = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k

⋀1≤j≤n⋀1≤k≤n [j≠k] ∀z:o ¬(CEj(z) ∧ CEk(z))

+?mileage may be optimized?! see diff 🌩️

DisjointUnion( C CE1 ... CEn )

(C)C = (CE1)C ∪ ... ∪ (CEn)C and

(CEj)C ∩ (CEk)C = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k

EquivalentClasses(C ObjectUnionOf(CE1 ... CEn))

∧ DisjointClasses(CE1 ... CEn)



пт, 15 авг. 2025 г. в 19:12, Michael DeBellis <[email protected]>:

> I don't use OWL Functional Syntax much but below is my best shot. I'm
> using an ontology called the People Ontology as my test case. This is an
> ontology I've been using to train clients on OWL because you can do things
> with property hierarchies that are powerful and intuitive and in my
> experience property hierarchies are one of the things new users get most
> confused about.
>
> Because I may be getting some of the functional syntax wrong here's some
> of the things I'm trying to model:
>
> Gender is a defined enumerated class with definition: {Male, Female,
> Non_Binary}
> Adult is a defined class with definition: Person and ('has age' some
> xsd:integer[>= 18])
> Hermit is a defined class with definition: Person and ('has social
> connection' exactly 0 Person)
>
> Also, this isn't that critical an issue. For the use case I have whether
> Male, Female, and Non_Binary are logically in the TBox or ABox doesn't
> matter. The use case is I want to put entities in different graphs so that
> I can keep data and terminology separate and can extract the terminology
> (the ontology without all the data) and to do that I clearly need to have
> all those definitions above. The main things I was wondering were: 1) In
> terms of the OWL specification are all those in the TBox? I thought they
> weren't but it seems Samson thinks they are (for the same reason that I
> thought they should be) but Alex thinks they aren't. 2) When I write this
> up should I use the terms TBox and ABox or something else? I'm leaning
> pretty heavily to using those terms with a little note that clarifies that
> by strict Description Logic a few of these entities aren't in the TBox but
> since we need them to have the complete ontology definition we're going to
> put them in the TBox subgraph. Hope that makes sense, here's my attempt at
> OWL Functional Syntax:
>
> Prefix(:=<http://michaeldebellis.com/people/>)
> Prefix(xsd:=<http://www.w3.org/2001/XMLSchema#>)
> Ontology(
>
>   # --- Declarations  ---
>   Declaration(Class(:Gender))
>   Declaration(Class(:Adult))
>   Declaration(Class(:Human))
>   Declaration(Class(:Person))
>
>   Declaration(ObjectProperty(:has_social_connection))
>   Declaration(DataProperty(:has_age))
>
>   Declaration(NamedIndividual(:Male))
>   Declaration(NamedIndividual(:Female))
>   Declaration(NamedIndividual(:Non_Binary))
>
>   # --- 1) Gender ≡ {Male, Female, Non_Binary} ---
>   EquivalentClasses(
>     :Gender
>     ObjectOneOf(:Male :Female :Non_Binary)
>   )
>
>   # (Optional but redundant, entailed by the axiom above)
>   # ClassAssertion(:Gender :Male)
>   # ClassAssertion(:Gender :Female)
>   # ClassAssertion(:Gender :Non_Binary)
>
>   # --- 2) Adult ≡ Human ⊓ (has_age some xsd:integer[>=18]) ---
>   EquivalentClasses(
>     :Adult
>     ObjectIntersectionOf(
>       :Human
>       DataSomeValuesFrom(
>         :has_age
>         DatatypeRestriction(xsd:integer xsd:minInclusive "18"^^xsd:integer)
>       )
>     )
>   )
>
>   # --- 3) Hermit ≡ Person ⊓ (has_social_connection exactly 0 Person) ---
>   EquivalentClasses(
>     :Hermit
>     ObjectIntersectionOf(
>       :Person
>       ObjectExactCardinality(0 :has_social_connection :Person)
>     )
>   )
> )
>
> On Fri, Aug 15, 2025 at 3:06 AM Alex Shkotin <[email protected]>
> wrote:
>
>> My five pence:
>>
>> The formal definition is as follows:
>>
>> Tbox - axioms of the form in Tables 1,3-9.
>>
>> Abox - axioms of the form in Table 10.
>>
>> Tables see OWL 2 Web Ontology Language Direct Semantics (Second Edition)
>> <https://www.w3.org/TR/owl2-semantics/> or OWL 2 Functional Style
>> operators from HOL point of view
>> <https://www.researchgate.net/publication/336363623_OWL_2_Functional_Style_operators_from_HOL_point_of_view>
>> .
>>
>> If MDB rewrites his examples in OWL2 Functional style we can classify
>> them properly.
>>
>> If we compare with FOL or HOL, a constant of the theory is a very
>> important term but it goes to Abox.
>>
>> If in the ontology we store a theory and a structure that satisfies this
>> theory, then the data axioms (tables 3, 7–9) should probably be
>> separated into Dbox (narrowing Tbox)⛈️
>>
>> Alex
>>
>>
>> пт, 15 авг. 2025 г. в 01:03, Michael DeBellis <[email protected]>:
>>
>>> I've seen a few users in the past ask about ways to separate TBox from
>>> ABox and I've wanted to do that myself. For me it is mostly to be able to
>>> keep using Protege even when the amount of data is so large that it isn't
>>> practical to load the complete graph into Protege.
>>>
>>> I've been trying to write some SPARQL to do this and there are two
>>> issues I was wondering about: Enumerated Classes and Puns. Should these be
>>> in the TBox or ABox? Conceptually, it seems to me that in both cases these
>>> are about the Terminology not data so they belong in the TBox, but I think
>>> technically since they are still instances they probably go in the ABox.
>>>
>>> E.g., in my version of the Pizza tutorial there is an enumerated class
>>> called Spiciness with the definition: {Hot, Medium, Mild}. Those values
>>> aren't data, they are ways to tag Pizzas into different categories along
>>> the Spiciness dimension. Also, for the use cases I have in mind, I would
>>> definitely want those to be included in the excerpt from a big knowledge
>>> graph that I wanted to load into Protege, because what I want to do is view
>>> and possibly edit the model without the data and the model won't be correct
>>> without the individuals that define any enumerated classes.
>>>
>>> Similarly for puns. Yes, they are instances and they do hold data but
>>> the data isn't for any specific individual it can represent all sorts of
>>> things like metadata or default values but in all use cases that I can
>>> think of it seems to me the puns belong in the TBox but my guess is that
>>> the official answer would be they are instances and instances go in the
>>> ABox.
>>>
>>> Actually, as I think about it, this could come up in other ways too.
>>> E.g., once I had classes that were organized based on the state they were
>>> in. E.g., classes like California_Data, Illionois_Data and they had axioms
>>> like "has_state value California" or if we define an Adult as a Person
>>> whose age is equal to or greater than the xsd:decimal 18 those definitions
>>> and the numbers should also be in the TBox, even though normally an
>>> xsd:decimal would be in the ABox.
>>>
>>> Michael
>>> https://www.michaeldebellis.com/blog
>>> _______________________________________________
>>> protege-user mailing list
>>> [email protected]
>>> https://mailman.stanford.edu/mailman/listinfo/protege-user
>>>
>> _______________________________________________
>> protege-user mailing list
>> [email protected]
>> https://mailman.stanford.edu/mailman/listinfo/protege-user
>>
> _______________________________________________
> protege-user mailing list
> [email protected]
> https://mailman.stanford.edu/mailman/listinfo/protege-user
>

_______________________________________________
protege-user mailing list
[email protected]
https://mailman.stanford.edu/mailman/listinfo/protege-user