David R. Koepsell

Formal Ontology · BFO · OWL DL · Reasoner-Validated

Ontologies a reasoner has checked.

Four connected pieces of work, each grounded in the Basic Formal Ontology and validated against an OWL DL reasoner: BFO-Agent, which populates an ontology from source text and commits only assertions the reasoner accepts; the FOL / OWL Tester, which finds the consistency and coherence faults that pass silently in standard editors; A Structural Ontology of the Law, a 6,900-class formalization of legal structure; and a public library of validated ontologies. What each one does, and what it is for, follows.

BFO-Agent · validation-gated pipeline LLM proposes · OWL reasoner commits
LM EXTRACTION proposes candidate axiom BFO · OWL REASONER consistent & entailed? upper-ontology + DL check COMMITTED with provenance to source × NOT COMMITTED logged, kept out of the KB
93.3%
of unfounded assertions refused under the gate, across three public corpora
10%
refused at the ungated baseline, on identical inputs
3
validated corpora in the evaluation: SOoL, Spinoza, Leibniz

§ 01 — BFO-Agent

Populating an ontology from text, without confabulation

BFO-Agent separates proposal from commitment. A language model, LoRA fine-tuned for extraction, reads a source text and proposes candidate axioms. Each candidate is evaluated against the BFO upper ontology and tested for logical consistency and entailment by an OWL DL reasoner. Axioms that pass are committed to the knowledge base with a provenance link back to the source span that produced them. Axioms that fail are logged and never enter the ontology.

The agent is reflexive: it evaluates its own proposed commitments rather than treating its output as authoritative, which is the mechanism by which it declines instead of inventing. The refusal behavior is a property of the pipeline, not of the prompt.

Measured: 93.3% refusal of unfounded assertions under the gate vs. 10% at the ungated baseline, on identical inputs, across SOoL, Spinoza’s Ethics, and the Leibniz corpus. Reported in “Confabulation is Architectural” (under review, Minds and Machines).

What it is for Point it at a corpus and receive a BFO-aligned ontology in which every class and relation is reasoner-consistent and traceable to the text that justified it. It removes the manual audit step that makes LLM-assisted ontology population untrustworthy.
validation-gated BFO upper ontology OWL DL reasoner reflexive LoRA fine-tuned provenance-tracked
  • proposeExtraction model reads source text and emits candidate axioms. None are yet committed.
  • gateEach candidate is checked against BFO and tested for consistency and entailment by the reasoner.
  • commitPassing axioms enter the KB, each with a provenance link to its source span.
  • logFailing candidates are recorded and excluded. Exclusion is the default for anything unproven.

§ 02 — FOL / OWL Tester

Finding the faults editors pass over

An OWL ontology can look correct in an editor and still reason wrong. The Tester loads an OWL or RDF ontology and runs three checks. Consistency: a description-logic test of whether the axioms admit any model at all. Coherence: detection of category errors against the BFO backbone, including partition-straddle, where a class is entailed to be both a continuant and an occurrent, violating BFO’s top-level disjointness. Entailment: a first-order test of what the axioms actually imply, as opposed to what the author intended.

Partition-straddle is the representative case. It produces no warning in Protégé or most editors, yet it corrupts every inference that touches the affected class. As a concrete instance, the Tester flagged an aerospace ontology in which Force, Weight, Drag, and Lift were each entailed to straddle the continuant/occurrent partition.

What it is for It catches structural defects before they reach a reasoner in production, and it lets students watch an ontology fail under a reasoner, which teaches description-logic semantics faster than any lecture on them.
OWL / RDF description logic first-order logic BFO coherence teaching tool
  • consistencyDL check of whether the ontology admits a model at all.
  • coherenceDetects partition-straddle and category errors against the BFO backbone.
  • entailmentTests what the axioms actually imply, not what was intended.
  • pedagogySelf-contained exercises that make failure visible to students.

§ 03 — A Structural Ontology of the Law

A Structural Ontology of the Law

The largest application of the method. Law is formalized not as a body of language but as a structured region of social reality: roles, authorities, recognitions, obligations, powers, and the specific ways each can fail. The released ontology runs to nearly 6,900 classes, BFO-aligned and validated for consistency with the HermiT reasoner.

It supplies three constructs the rest of the work builds on: the eight-node Minimum Legal Chain, which a legal scenario can be walked through to test for closure; a thirteen-type contradiction typology; and the Irreversible Accountability Test. A legal system fails, on this account, when recognitions misalign or obligations lose their correlates, producing contradiction debt that has to be repaired.

What it is for A queryable, reasoner-checked model of legal structure that drives the MLC Chain Auditor, supports jurisprudence and AI-and-law teaching, and gives downstream legal-reasoning tools a formal backbone rather than an informal taxonomy.

Forthcoming · Palgrave Macmillan · 2026

§ 04 — The Ontology Library

Public ontologies, reasoner-validated

Each ontology renders a body of thought into BFO and is validated for consistency with the HermiT reasoner. All are browsable, citable, and free, and each was built with BFO-Agent. Each one doubles as a reusable BFO module and as a worked reference for how a given source maps onto a formal upper ontology.

§ 05 — Custom Ontologies

Developing a custom ontology for a domain

The same method that produced the library applies to any domain. The process is fixed and reasoner-checked at every stage. Analysis: identify the continuants, occurrents, roles, dispositions, and relations the domain actually contains. Alignment: map them onto the BFO upper ontology so the model inherits a principled backbone rather than an ad hoc hierarchy. Formalization: express the result in OWL DL. Validation: run consistency and coherence checks until the reasoner accepts the model. Provenance and documentation: deliver it as a modular, traceable, queryable artifact.

The result is not a diagram or a glossary. It is a logical model a reasoner has accepted, which is what makes the value below available rather than aspirational.

Value — what a validated ontology buys

  • semanticsOne explicit, machine-checkable definition per term, replacing the conflicting definitions scattered across spreadsheets, schemas, and documents.
  • interoperabilityBFO alignment connects the model to the wider BFO and OBO ecosystem and lets data integrate across systems that previously could not be joined.
  • inferenceA reasoner derives implied facts and answers queries a relational schema cannot express, turning a vocabulary into something that computes.
  • consistencyContradictions surface at design time, when the reasoner refuses the model, rather than in production where they corrupt results.
  • auditabilityProvenance and formal definitions make the model traceable and defensible under scrutiny.

§ 06 — Consulting

Engagements

I take on formal-ontology and ontology-grounded-AI work for research groups, standards efforts, and teams whose data models have outgrown the schema they started in. Trained in formal ontology under Barry Smith, one of the founders of BFO. Engagements take one of these forms, and most combine several.

Custom ontology development

Build a domain ontology from analysis through BFO-aligned, reasoner-validated OWL, delivered with provenance and documentation.

BFO conformance audit

Map an existing ontology to BFO and report where it straddles partitions, contradicts itself, or fails to entail what it claims.

Coherence diagnostics

Run a live ontology through consistency and partition checks and return a defect report scoped to what to fix and why.

Validation tooling & LLM pipelines

Build the validators and reasoner-gated pipelines, on the BFO-Agent pattern, that keep unfounded assertions out of a knowledge base.