- Validate BFO based ontologies against BFO FOL
- Compare theorem prover performance OWL vs FOL
- Compare satisfiability performance OWL vs FOL
- Compare concept satisfiability (coherence?) of OWL vs FOL.
- check whether all classes in an ontology may be instantiated at the same time.
- Support heterogenous OWL / FOL modelling with OWL annotations
- Theoretical question: What FOL formulas may be to OWL added, while still guaranteeing consistency. (Motivation: OWL consistency checking is easy, FOL consistency checking is hard. Hence, if we could show that the consistency is preserved, it would make heterogenous modelling better)
- Theory Interpolation approximating FOL in OWL.
- Generating an OWL proof (= justification in OWL, axiom pinpointing) a FOL proof.