Upper Ontology Specification¶

Abstract¶

This document specifies the upper ontology for Mistaber, comprising 29 sorts organized across physical, normative, and classification domains. We formalize the sort system using Description Logic notation, providing TBox axioms that define sort relationships, disjointness constraints, and domain/range restrictions. The ontology enforces both Closed World Assumption (CWA) for factual predicates and Open World Assumption (OWA) for derived normative conclusions. We prove key properties including sort disjointness, subsumption completeness, and constraint satisfaction.

1. Introduction¶

1.1 Motivation¶

Halachic reasoning operates over a rich domain of entities: foods, vessels, actions, rules, authorities, and normative statuses. A formal ontology provides:

Type Safety: Ensuring predicates receive arguments of appropriate sorts
Inference Support: Enabling subsumption-based reasoning
Consistency Checking: Preventing invalid combinations (e.g., food being both meat and dairy)
Interoperability: Potential alignment with standard upper ontologies (BFO, DOLCE)

1.2 Contribution¶

We provide:

A three-domain sort hierarchy (physical, normative, classification)
Formal TBox axioms in Description Logic notation
Disjointness constraints with soundness proofs
Domain and range restrictions for all predicates
CWA/OWA annotations distinguishing factual from derived predicates

2. Preliminaries¶

2.1 Description Logic Notation¶

Definition 2.1 (ALC Syntax). The Attributive Language with Complements (ALC) provides: - Concept names: A, B, C (representing sorts) - Role names: R, S (representing binary relations) - Constructors: - ⊤ (top/universal concept) - ⊥ (bottom/empty concept) - ¬C (complement) - C ⊓ D (intersection) - C ⊔ D (union) - ∃R.C (existential restriction) - ∀R.C (universal restriction)

Definition 2.2 (TBox). A TBox is a set of concept inclusions: $$C ⊑ D \quad \text{(C is subsumed by D)}$$

Definition 2.3 (ABox). An ABox is a set of concept and role assertions: - C(a): Individual a is of type C - R(a, b): Individuals a and b are related by R

2.2 Open vs. Closed World Assumption¶

Definition 2.4 (Closed World Assumption). Under CWA, absence of assertion implies negation: $$\text{If } A(x) \text{ not asserted, then } ¬A(x)$$

Definition 2.5 (Open World Assumption). Under OWA, absence of assertion implies unknown: $$\text{If } A(x) \text{ not asserted, then truth value of } A(x) \text{ is undetermined}$$

Mistaber uses CWA for factual predicates (food types, temperatures) and OWA for normative conclusions (permitted, forbidden).

3. Sort Hierarchy¶

3.1 Top-Level Domains¶

Definition 3.1 (Domain Partition). The universe of discourse partitions into three disjoint domains: $$\mathcal{U} = Physical ⊔ Normative ⊔ Classification$$

where: - Physical: Tangible entities (foods, vessels, mixtures) - Normative: Abstract halachic entities (rules, worlds, authorities) - Classification: Enumerated type values (categories, statuses)

3.2 Physical Domain Sorts¶

Definition 3.2 (Physical Sorts). The physical domain comprises:

Sort	Description	Subsumes
`food`	Edible substances	-
`vessel`	Containers (kelim)	-
`mixture`	Combined foods	-
`action`	Physical actions	-
`agent`	Entities performing actions	-
`time_point`	Temporal instants	-
`location`	Physical places	-
`quantity`	Numeric measurements	-

Axiom 3.1 (Physical Disjointness). $$food ⊓ vessel = ⊥$$ $$food ⊓ mixture = ⊥$$ $$vessel ⊓ mixture = ⊥$$ $$action ⊓ agent = ⊥$$

Note: A mixture may contain foods but is not itself a food in the primitive sense.

3.3 Normative Domain Sorts¶

Definition 3.3 (Normative Sorts). The normative domain comprises:

Sort	Description	Subsumes
`issue`	Halachic questions	-
`ruling`	Halachic determinations	-
`rule_id`	Formal rule identifiers	-
`source_ref`	Citations to sources	-
`posek`	Halachic authorities	-
`world`	Possible worlds (traditions)	-
`policy`	Configuration settings	-

Axiom 3.2 (Normative Disjointness). $$world ⊓ rule_id = ⊥$$ $$posek ⊓ world = ⊥$$ $$source_ref ⊓ rule_id = ⊥$$

3.4 Classification Domain Sorts¶

Definition 3.4 (Classification Sorts). Enumerated types for categorization:

Sort	Values	Domain
`food_category`	maakhal, basar, chalav, parve, beheima, chaya, of, dag, mashkeh, tavlin	food
`action_type`	achiila, bishul, hanaah	action
`issur_type`	achiila, hanaah, bishul, taarovet, kli	prohibition
`temp_status`	tzonen, cham, roteiach	food
`kli_status`	kli_rishon, kli_sheni, kli_shlishi	vessel
`madrega_type`	d_oraita, d_rabanan, minhag, chumra	rule
`status_type`	assur, mutar, chiyuv, reshut, mitzvah, sakanah	conclusion
`stringency_level`	lechatchila, bediavad	application
`shiur_type`	k_zayit, k_beitza, shishim, noten_taam	measurement
`context`	ctx_normal, ctx_hefsed, ctx_shaat_hadchak	situation
`policy_type`	minhag_region, chumra_level, safek_treatment, shiur_standard, bitul_threshold	configuration

4. TBox Axioms¶

4.1 Food Category Hierarchy¶

Definition 4.1 (Food Category Subsumption).

maakhal ⊑ food_category
basar ⊑ maakhal
chalav ⊑ maakhal
parve ⊑ maakhal

beheima ⊑ basar
chaya ⊑ basar
of ⊑ basar
dag ⊑ basar

mashkeh ⊑ maakhal
tavlin ⊑ maakhal

Theorem 4.1 (Food Category Partition). At the top level, food categories partition maakhal: $$maakhal ≡ basar ⊔ chalav ⊔ parve$$

Proof. Every food item must be classified as meat, dairy, or neutral. The constraint:

:- food(F),
   not food_type(F, basar),
   not food_type(F, chalav),
   not food_type(F, parve),
   not classification_unknown(F).

ensures exhaustiveness. Disjointness constraints (Section 5) ensure mutual exclusion. □

4.2 Meat Subcategory Axioms¶

Axiom 4.1 (Meat Subcategory Disjointness). $$beheima ⊓ chaya = ⊥$$ $$beheima ⊓ of = ⊥$$ $$beheima ⊓ dag = ⊥$$ $$chaya ⊓ of = ⊥$$ $$chaya ⊓ dag = ⊥$$ $$of ⊓ dag = ⊥$$

Definition 4.2 (Meat Subcategory Coverage). $$basar ≡ beheima ⊔ chaya ⊔ of ⊔ dag$$

Note: While fish (dag) is halachically classified under basar for some purposes, its unique status regarding basar bechalav is captured through specific rules rather than ontological classification.

4.3 Temperature State Axioms¶

Axiom 4.2 (Temperature Mutual Exclusion). $$tzonen ⊓ cham = ⊥$$ $$tzonen ⊓ roteiach = ⊥$$ $$cham ⊓ roteiach = ⊥$$

Axiom 4.3 (Temperature Ordering). Implicit ordering via definitions: $$roteiach → heated$$ $$cham → heated$$ $$tzonen → ¬heated$$

4.4 Madrega Axioms¶

Axiom 4.4 (Madrega Total Ordering). The madrega types form a total order: $$d_oraita > d_rabanan > minhag > chumra$$

Encoded via stronger/2 relation with transitive closure.

Axiom 4.5 (Madrega Functional Dependency). Each rule has exactly one madrega: $$∀r: rule(r) → ∃!m: madrega(r, m)$$

5. Disjointness Constraints¶

5.1 Formal Constraint Specification¶

Definition 5.1 (Disjointness Constraint). Sorts A and B are disjoint iff: $$A ⊓ B = ⊥ \quad \text{equivalently} \quad ∀x: ¬(A(x) ∧ B(x))$$

5.2 Food Classification Constraints¶

Constraint 5.1 (Top-Level Food Exclusivity).

:- food_type(F, basar), food_type(F, chalav).
:- food_type(F, basar), food_type(F, parve).
:- food_type(F, chalav), food_type(F, parve).

Theorem 5.1 (Food Classification Soundness). No stable model exists where a food has multiple top-level classifications.

Proof. By integrity constraint semantics in ASP, any model containing both food_type(f, basar) and food_type(f, chalav) for some f would satisfy the body of the constraint :- food_type(F, basar), food_type(F, chalav), making the model unstable. □

5.3 Temperature Constraints¶

Constraint 5.2 (Temperature Exclusivity).

:- temperature(F, tzonen), temperature(F, cham).
:- temperature(F, tzonen), temperature(F, roteiach).
:- temperature(F, cham), temperature(F, roteiach).

5.4 Normative Status Constraints¶

Constraint 5.3 (Status Exclusivity).

:- forbidden(W, A, F, C), permitted(W, A, F, C).

Theorem 5.2 (Normative Consistency). For any world w, action a, food f, and context c: $$¬(forbidden(w, a, f, c) ∧ permitted(w, a, f, c))$$

Proof. Direct consequence of Constraint 5.3. The integrity constraint eliminates any model containing both atoms. □

6. Domain and Range Restrictions¶

6.1 Predicate Signatures¶

Definition 6.1 (Predicate Signature). A signature σ(P) = ⟨S₁, ..., Sₙ⟩ specifies that predicate P of arity n requires its i-th argument to be of sort Sᵢ.

6.2 Core Predicate Signatures¶

Predicate	Signature	Description
`food/1`	⟨food⟩	Entity is a food
`vessel/1`	⟨vessel⟩	Entity is a vessel
`mixture/1`	⟨mixture⟩	Entity is a mixture
`food_type/2`	⟨food, food_category⟩	Food has category
`temperature/2`	⟨food, temp_status⟩	Food has temperature
`contains/2`	⟨mixture, food⟩	Mixture contains food
`world/1`	⟨world⟩	Entity is a world
`accessible/2`	⟨world, world⟩	Accessibility relation
`rule/1`	⟨rule_id⟩	Entity is a rule
`madrega/2`	⟨rule_id, madrega_type⟩	Rule has normative level
`scope/2`	⟨rule_id, world⟩	Rule scoped to world
`makor/2`	⟨rule_id, source_ref⟩	Rule has source
`forbidden/4`	⟨world, action_type, food, context⟩	Normative prohibition
`permitted/4`	⟨world, action_type, food, context⟩	Normative permission

6.3 Type Checking Constraints¶

Constraint 6.1 (Valid Action Type).

:- forbidden(_, A, _, _), not action_type(A).
:- permitted(_, A, _, _), not action_type(A).

Constraint 6.2 (Valid Context Type).

:- forbidden(_, _, _, C), not context_type(C).
:- permitted(_, _, _, C), not context_type(C).

Constraint 6.3 (Valid Madrega Type).

:- madrega(_, M), not madrega_type(M).

7. CWA/OWA Annotations¶

7.1 Closed World Predicates¶

Definition 7.1 (CWA Predicate). A predicate P is under CWA iff: $$¬P(x) \text{ if } P(x) \text{ not derivable}$$

The following predicates operate under CWA:

Predicate	Rationale
`food/1`	Only explicitly declared foods exist
`vessel/1`	Only explicitly declared vessels exist
`mixture/1`	Only explicitly declared mixtures exist
`food_type/2`	Classification must be explicit
`temperature/2`	Physical state must be declared
`contains/2`	Mixture contents must be explicit
`world/1`	Only declared worlds exist
`rule/1`	Only declared rules exist
`makor/2`	Sources must be explicit

7.2 Open World Predicates¶

Definition 7.2 (OWA Predicate). A predicate P is under OWA iff: $$P(x) \text{ undetermined if neither } P(x) \text{ nor } ¬P(x) \text{ derivable}$$

The following predicates operate under OWA:

Predicate	Rationale
`permitted/4`	May be derived or undetermined
`forbidden/4`	May be derived or undetermined
`is_kosher/1`	Absence doesn't imply non-kosher
`holds/2`	Propositions may be undetermined

7.3 Safek and OWA¶

The Open World Assumption is essential for handling safek (uncertainty). When a food's type is unknown:

unknown(food_type, F) :-
    food(F),
    not known_food_type(F).

Under CWA, not known_food_type(F) would immediately imply the food has no type. Under OWA for derived conclusions, we can propagate this uncertainty to safek status (see Document 05).

8. Structural Properties¶

8.1 Sort Partition Theorem¶

Theorem 8.1 (Domain Partition). Every entity in the universe belongs to exactly one top-level domain: $$∀x ∈ \mathcal{U}: (Physical(x) ⊕ Normative(x) ⊕ Classification(x))$$

where ⊕ denotes exclusive or.

Proof. By construction, predicates are defined to accept only specific sort arguments. Type checking constraints (Section 6.3) ensure no entity can satisfy predicates from multiple domains. □

8.2 Subsumption Completeness¶

Theorem 8.2 (Subsumption Completeness). The subcategory_of/2 relation is the reflexive-transitive closure of subcategory/2: $$subcategory_of(X, Y) \text{ iff } X = Y \text{ or } ∃Z: subcategory(X, Z) ∧ subcategory_of(Z, Y)$$

Proof. By definition in sorts.lp:

subcategory_of(X, Y) :- subcategory(X, Y).
subcategory_of(X, Z) :- subcategory(X, Y), subcategory_of(Y, Z).

The base case provides direct subsumption; the recursive case provides transitivity. Reflexivity is implicit through the base case when the direct edge exists. □

8.3 Constraint Satisfaction¶

Theorem 8.3 (Model Consistency). Every stable model of Mistaber satisfies all disjointness constraints.

Proof. ASP semantics guarantee that integrity constraints (rules with empty heads) eliminate any model that satisfies the constraint body. Each disjointness axiom is encoded as an integrity constraint. Therefore, no stable model can violate disjointness. □

9. Implementation Notes¶

9.1 Sort Declarations¶

File: mistaber/ontology/schema/sorts.lp

% Physical domain sorts
#defined food/1.
#defined vessel/1.
#defined mixture/1.

% Normative domain sorts
#defined world/1.
#defined rule/1.
#defined posek/1.

% Food categories
food_category(maakhal).
food_category(basar).
food_category(chalav).
food_category(parve).
% ... etc.

% Hierarchy
subcategory(basar, maakhal).
subcategory(chalav, maakhal).
subcategory(parve, maakhal).
subcategory(beheima, basar).
% ... etc.

9.2 Disjointness Constraints¶

File: mistaber/ontology/schema/disjointness.lp

% Food classification is mutually exclusive at top level
:- food_type(F, basar), food_type(F, chalav).
:- food_type(F, basar), food_type(F, parve).
:- food_type(F, chalav), food_type(F, parve).

% Subcategories are mutually exclusive within meat
:- food_type(F, beheima), food_type(F, chaya).
% ... etc.

9.3 Integrity Constraints¶

File: mistaber/ontology/schema/constraints.lp

% Every food must have classification (unless explicitly unknown)
:- food(F),
   not food_type(F, basar),
   not food_type(F, chalav),
   not food_type(F, parve),
   not classification_unknown(F).

% Rules must have sources
:- rule(R), not has_makor(R).
has_makor(R) :- rule(R), makor(R, _).

9.4 Vocabulary Registry¶

File: mistaber/dsl/vocabulary/base.yaml

The YAML registry provides machine-readable sort and predicate definitions:

sorts:
  - food
  - vessel
  - mixture
  # ... etc.

predicates:
  - name: food_type
    arity: 2
    signature: [food, food_category]
    cwa: true

The Mistaber ontology draws from:

Upper ontology design principles (Guarino, 1998)
Legal ontologies (Hoekstra et al., 2007)
Food ontologies (Dooley et al., 2018)

See Appendix A for mappings to BFO and DOLCE.

References¶

Guarino, N. (1998). Formal Ontology and Information Systems. Proceedings of FOIS'98, 3-15.
Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., & Patel-Schneider, P.F. (Eds.). (2003). The Description Logic Handbook. Cambridge University Press.
Hoekstra, R., Breuker, J., Di Bello, M., & Boer, A. (2007). The LKIF Core Ontology of Basic Legal Concepts. Proceedings of LOAIT 2007.
Dooley, D.M., et al. (2018). FoodOn: A Harmonized Food Ontology to Increase Global Food Traceability, Quality Control and Data Integration. npj Science of Food, 2(1), 23.
Niles, I., & Pease, A. (2001). Towards a Standard Upper Ontology. Proceedings of FOIS 2001.