Scope

ff-owl formalizes the OWL 2 ontology language in Agda, covering raw syntax, checked and portable representations, and direct semantics. Its module hierarchy follows elaboration from declarations and imports through symbol tables, punning, and structural checks into kernels and semantic interpretations. It models global restrictions on object properties—including property kinds, chains, regularity, cardinality, and keys—alongside XML Schema datatypes and the OWL EL, QL, and RL profiles. It also connects JSON-shaped OBOGraph documents to OWL through schema decoding, reference resolution, validation, policy, conversion, and reporting. Corpus and example modules exercise accepted and rejected inputs, countermodels, family ontologies, WebProtégé use cases, and multi-document import projects.

Most important results

The direct-semantics development defines interpretations, ontology semantics, entailment, datatype handling, annotation erasure, expansions, and supporting lemmas. The portable regularity and regularity-rank developments connect object-property restriction checks to explicit proofs, while related checkers cover declarations, property roles, semantic support, and WebProtégé policy. The OBOGraph pipeline decodes JSON, validates schemas, references, and policies, converts accepted graphs into a portable ontology representation, and produces structured reports. Import-closure, checked-import, kernel-morphism, and semantic import-project modules provide a path for relating multi-document ontologies to checked kernels and their meanings.