Skip to main content

OWL 2 reasoning — Pizza ontology end-to-end

This recipe shows the full OWL 2 stack against a small concrete ontology — Verum's analogue of the Manchester Pizza Ontology that Protégé / Pellet / HermiT users know from training material. The ontology fits in one file, runs through verum audit --owl2-classify to produce a class hierarchy, and is consumed by @verify(formal) for downstream reasoning.

For the underlying framework see Verification → OWL 2 integration; for the full attribute family see stdlib → theory interop.

1. The ontology​

mount core.math.frameworks.owl2_fs.*;

// =================================================================
// Class hierarchy
// =================================================================

@owl2_class
public type Food is { name: Text };

@owl2_class
@owl2_subclass_of(Food)
public type Pizza is { base: Text, toppings: List<Text> };

@owl2_class
@owl2_subclass_of(Pizza)
public type VegetarianPizza is { base: Text, toppings: List<Text> };

@owl2_class
@owl2_subclass_of(Pizza)
public type CheesyPizza is { base: Text, toppings: List<Text> };

@owl2_class
@owl2_subclass_of(VegetarianPizza)
@owl2_subclass_of(CheesyPizza)
public type Margherita is { base: Text, toppings: List<Text> };

// =================================================================
// Disjointness
// =================================================================

@owl2_class
@owl2_subclass_of(Pizza)
@owl2_disjoint_with([VegetarianPizza])
public type MeatPizza is { base: Text, toppings: List<Text> };

// =================================================================
// Properties
// =================================================================

@owl2_property(domain = Pizza, range = Topping,
               characteristic = [InverseFunctional])
public fn has_topping(p: Pizza, t: Topping) -> Bool { ... }

@owl2_class
public type Topping is { name: Text };

@owl2_class
@owl2_subclass_of(Topping)
public type VegetarianTopping is { name: Text };

@owl2_class
@owl2_subclass_of(Topping)
@owl2_disjoint_with([VegetarianTopping])
public type MeatTopping is { name: Text };

// =================================================================
// Identification key
// =================================================================

@owl2_class
@owl2_has_key(name)
public type NamedThing is { name: Text };

2. Run the classifier​

$ verum audit --owl2-classify
        --> Computing OWL 2 classification hierarchy

  ▸ Classes (with full ancestor closure)
    · Food
    · Pizza            ⊑ Food
    · VegetarianPizza  ⊑ Pizza, Food
    · CheesyPizza      ⊑ Pizza, Food
    · Margherita       ⊑ VegetarianPizza, CheesyPizza, Pizza, Food
    · MeatPizza        ⊑ Pizza, Food
    · Topping
    · VegetarianTopping ⊑ Topping
    · MeatTopping      ⊑ Topping
    · NamedThing       (key: [name])

  ▸ Disjointness pairs
    · MeatPizza        ⊥ VegetarianPizza
    · MeatTopping      ⊥ VegetarianTopping

  ▸ Object properties
    · has_topping  Pizza → Topping  [InverseFunctional]

  10 classes  ·  1 property  ·  2 disjointness pairs
  graph audit: load-bearing

Margherita's ancestor closure includes VegetarianPizza and CheesyPizza because both were declared as direct parents — the classifier walks the transitive closure deterministically (BTreeSet ordering for CI-friendly diffs).

3. Consistency check​

A consistency violation surfaces at compile time. If we add:

@owl2_class
@owl2_subclass_of(MeatPizza)
@owl2_subclass_of(VegetarianPizza)
public type Paradox is { ... };

…the audit reports:

error[ATS-V-AP-023]: framework-axiom collision
  --> Paradox.vr:1
   |
   | Paradox is declared as subclass of both MeatPizza and
   | VegetarianPizza, which are explicitly Disjoint.
   | The class extension would be empty under any model that
   | satisfies the disjointness assertion, contradicting the
   | implicit non-emptiness of any declared class.
   |
help: drop one of the parent declarations or remove the
      DisjointClasses assertion if both pizza kinds are
      meant to overlap.

The violation is caught by AP-023 FoundationForgery; no runtime check is generated.

4. Subsumption query​

@verify(formal)
public fn is_vegetarian(p: Pizza) -> Bool
    where ensures (result == true => p is VegetarianPizza)
{
    p is VegetarianPizza
}

The @verify(formal) discharge consults the OWL 2 framework axioms (the subClassOf / disjointClasses SMT encoding) plus Verum's value-level type checker. The post-condition result == true => p is VegetarianPizza is admitted by the SMT layer because VegetarianPizza ⊏ Pizza is in the framework axiom package — the proof is two lines of class-hierarchy lookup.

5. count_o on a finite domain​

When the universe is small and explicit, count_o runs at verification time:

mount core.math.frameworks.owl2_fs.count;

let pizzas: List<Pizza> = [margherita, four_cheese, pepperoni];

let veg_count: Int = count_o(pizzas, |p| p is VegetarianPizza);
// → 2 (margherita + four_cheese)

The witness (pizzas) is required at the call site — OWL 2 Direct Semantics is open-world per W3C §5.6, so Verum does not implicitly close the universe to perform cardinality reasoning.

For unbounded queries count_o_unbounded returns Maybe.None with E_OWL2_UNBOUNDED_COUNT as the diagnostic — unless the surrounding refinement type carries an explicit cardinality bound (e.g. {x : Int | x ≤ K ∧ x = count_o(_, P)}), in which case the verifier dispatches to SMT Finite Model Finding and recovers the count from the discovered finite model. See Verification → OWL 2 §5 for the dispatcher contract and the four-variant outcome (Decided / BoundExceeded / Unsupported / Timeout).

6. Round-trip with Protégé / HermiT / Pellet​

The same source exports to OWL 2 Functional-Style Syntax:

$ verum export --to owl2-fs pizza.vr
exported → pizza.ofn

The emitted pizza.ofn is consumable by Protégé, HermiT, Pellet, ELK, FaCT++, Konclude — every reasoner that speaks OWL 2 FS. Importing back is symmetric:

$ verum import --from owl2-fs pizza.ofn
imported → pizza.vr

Round-trip identity is verified at audit time via verum audit --round-trip --by-lineage owl2_fs. A faithful round-trip is the soundness premise for cross-tool inference agreement; the audit chronicle records the verdict per ontology.

7. Cross-references​