Prover9 and CLIF Formats
How this app exports ontologies to first-order logic, runs a theorem prover to cross-check the OWL reasoner, and accepts both syntaxes in the expression tester.
Overview
An OWL ontology describes classes and how they relate. To check that reasoning about it is sound, this app translates the ontology's structure into a first-order logic (FOL) theory and ships it to a theorem prover. If the prover and the OWL reasoner disagree about which classes are unsatisfiable, that points to a tool bug, which is exactly what a tester named FOL-BFO-OWL exists to catch.
Two FOL syntaxes are supported, side by side:
- Prover9 (LADR): a compact infix syntax read by the Prover9 theorem prover and the Mace4 model finder. This app runs both for the cross-check.
- CLIF (Common Logic Interchange Format): the ISO/IEC 24707 s-expression syntax. BFO 2020 (ISO/IEC 21838-2) is itself axiomatized in CLIF, so it is the natural interchange format for BFO work.
How membership is written (BFO 2020 temporalization)
BFO 2020 treats continuants and occurrents differently in time, so the export does too:
- Continuants (objects, qualities, dispositions, roles) persist through time, so membership is time indexed:
instance_of(x, C, t). - Occurrents (processes, events) carry their temporal parts intrinsically, so membership is atemporal:
instance_of_at(x, O).
A class is classified by whether it sits under BFO_0000002 (continuant) or BFO_0000003 (occurrent) in the vendored BFO catalog. A Wing instantiates at a time; a Flight does not.
Prover9 (LADR) syntax
| Construct | Prover9 |
|---|---|
| Universal quantifier | all X (...) |
| Existential quantifier | exists X (...) |
| And, Or | &, | |
| Implication, Biconditional | ->, <-> |
| Negation | - |
| Predicate | instance_of(X, force, T) |
| Clause terminator | a single . at the end of each formula |
Variables are capitalized (the export sets set(prolog_style_variables).); constants such as class names are lower case. Assumptions live inside a formulas(assumptions). ... end_of_list. block.
Worked example. If Force is placed under both Quality and Disposition (which BFO declares disjoint), the export is:
set(prolog_style_variables).
formulas(assumptions).
% --- Subsumptions (SubClassOf) ---
all X all T (instance_of(X,force,T) -> instance_of(X,disposition,T)).
all X all T (instance_of(X,force,T) -> instance_of(X,quality,T)).
% --- Disjointness ---
all X all T (-(instance_of(X,disposition,T) & instance_of(X,quality,T))).
end_of_list.To prove that Force is unsatisfiable, the cross-check adds the goal all X all T (-instance_of(X,force,T)). Prover9 negates it, assumes a force exists, and derives a contradiction through the disjointness axiom. A proof means the class is empty.
CLIF (Common Logic) syntax
| Construct | CLIF |
|---|---|
| Universal quantifier | (forall (x t) ...) |
| Existential quantifier | (exists (x) ...) |
| And, Or | (and ...), (or ...) |
| Implication, Biconditional | (if a b), (iff a b) |
| Negation | (not a) |
| Predicate | (instance_of x force t) |
| Module wrapper | (cl-text NAME form ...) |
The same Force example in CLIF:
(cl-text ontology-export
;; --- Subsumptions (SubClassOf) ---
(forall (x t) (if (instance_of x force t) (instance_of x disposition t)))
(forall (x t) (if (instance_of x force t) (instance_of x quality t)))
;; --- Disjointness ---
(forall (x t) (not (and (instance_of x disposition t) (instance_of x quality t)))))The official BFO 2020 CLIF axiomatization (13 normative modules from ISO/IEC 21838-2) is vendored with the app at bfo/bfo-2020.clif and used as the canonical statement of what BFO says.
Where you will find these in the app
1. On an analysis page (export and cross-check)
After you upload and analyze an ontology, the Provable FOL Export panel shows the theory in Prover9 and CLIF tabs, with download buttons. The Run prover cross-check button runs Prover9 and Mace4 over the export and compares the result with the OWL reasoner.
2. In the expression tester (input)
The FOL expression tester accepts Prover9 and CLIF directly. Paste either syntax and it is detected, converted to the internal form, validated, and checked against the BFO vocabulary. You do not need to rewrite expressions by hand.
Reading the cross-check verdict
| Verdict | Meaning |
|---|---|
| Agree | The prover and the OWL reasoner found the same set of unsatisfiable classes. Confidence is high. |
| Divergence | One tool flagged a class the other did not. The panel lists prover-only and reasoner-only classes. This is worth investigating: it can indicate a translation gap or a reasoner limitation. |
| Result without full agreement | The class count exceeded the per-run cap, so only a subset was tested. The number tested and the cap are reported. |
| Did not run | The Prover9 binary was not available on the server. The export still renders; only the live cross-check is skipped. |
The cross-check runs one prover invocation per class and is bounded by a time budget, so it is offered on demand rather than on every upload.
Running the export yourself
Download the Prover9 export and run it with Prover9 or Mace4 locally:
# Search for a proof (a contradiction implies an unsatisfiable theory):
prover9 -f ontology.p9
# Or look for a model (Mace4 confirms satisfiability):
mace4 -f ontology.p9The CLIF export can be loaded into any ISO Common Logic tool. Note that BFO 2020 CLIF is modular: it is a set of (cl-text ...) modules rather than one flat theory, matching the upstream structure.