TU Dresden  ◆  Faculty of Computer Science  ◆  Institute of Theoretical Computer Science  ◆  Chair of Automata Theory

ELK Certifier


Allows to generate certificates of classification results computed by the OWL EL reasoing system ELK. Such a certificate can be used by the proof checker LFSC to verify that the classification result contains no unsound inferences.

More information and technical details of the underlying methods can be found in the following publications:


F. Baader, P. Koopmann, and C. Tinelli: First Results on How to Certify Subsumptions Computed by the EL Reasoner ELK Using the Logical Framework with Side Conditions. In DL 2020: International Workshop on Description Logics, CEUR-WS. CEUR-WS.org, 2020. Link

The signature file for the proofs can be downloaded here:

Our implementation is available both as self-contained jar and as zip-file with the source code:

To compile the source code, you need the Scala Build Tool (SBT). A jar-file as above is then generated by executing "sbt assembly" in the source folder.


Usage

To test whether an ontology is in the supported fragment, use:

	java -cp elk-certifier-0.1.jar de.tu_dresden.lat.dlProofChecking.CheckSupported ONTOLOGY-FILE

To generate a certificate for the classification result for a given ontology as it is done in the paper, use:

	java -cp elk-certifier-0.1.jar de.tu_dresden.lat.dlProofChecking.GenerateClassificationCertificate ONTOLOGY-FILE