Over the past two decades, the Web Ontology Language (OWL) has been instrumental in advancing the development of ontologies and knowledge graphs, providing a structured framework that enhances the semantic integration of data. However, the reliability of deductive reasoning within these systems remains challenging, as evidenced by inconsistencies among popular reasoners in competitions. This evidence underscores the limitations of current testing-based methodologies, particularly in high-stakes domains such as healthcare. To mitigate these issues, in this study, we have developed VEL, a formally verified ℰ ℒ++ reasoner equipped with machine-checkable correctness proofs that ensure the validity of outputs across all possible inputs. This formalization, based on the algorithm of Baader et al.[1], has been transformed into executable OCaml code using the Coq proof assistant's extraction capabilities. In addition to producing a correct implementation, our work uncovered two errors in the published completeness proof that required a modification to the original algorithm.
CEUR ceur-ws.org
Knowledge graphs and ontologies can integrate diverse data sources semantically rigorously,
adhering to well-established W3C standards [
To address this problem, in this paper, we introduce VEL, a formally verified ℰ ℒ++ reasoner with machine-checkable correctness proofs. Our proofs ensure the correctness of the output https://www.koncordantlab.com/ (A. M. Ileri); https://www.koncordantlab.com/ (H. K. McGinty)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
for each possible input. We based our formalization on the algorithm of Baader et al. [
Baader et al. use automated theorem proving to certify the results of the ELK reasoner for OWL2
EL [
Hidalgo-Doblado et al. formalize ℒ description logic and implement a formally verified
tableau-based reasoner in PVS [
One challenging aspect of formalizing the language was formalizing concrete domains. We formalized concrete domains as a Coq record with six definitions: domain as a nonempty set of concrete domain elements, predicates as a set of predicate names, predicate arities as a partial function from predicate names to natural numbers, apply function that computes the application of a predicate, and satisfiability and implication functions that compute their respective properties between conjunctions of predicate expressions.
We formalized the provided model-theoretic semantics for ℰ ℒ++ . We first defined what we call a base interpretation which maps each name to its corresponding structure in the model. Then, we defined the interpretation function that recursively constructs the interpretation of a concept description for a given base interpretation.
Since normalization and classification use the same structure, namely, identifying a candidate and applying the appropriate rule, we followed the same pattern in their formalization. We formalized each rule in two parts: a predicate that encodes the condition and the application. In our implementations, we use a higher-order function to identify a candidate that satisfies a predicate, then apply the corresponding rule until no more candidates exist.
Defining a recursive function in Coq requires proving it is well-founded, i.e., it will terminate for all inputs. One way to do that is by providing a measure and proving that it decreases after each recursive call. A measure based on the number of rule applications left was suficient for most rules.
We had to make one modification to the normalization rule that applies to constraints of the form ⊓ ⊑ where or are complex concept descriptions. The termination measure does not decrease when the rule is applied to a constraint where both and are complex due to generating a new candidate. We circumvented this problem by applying the rule twice when both concept descriptions are complex.
We implemented strings and rational numbers as examples of concrete domains. Due to their complexity, we treated satisfiability and implication in those domains axiomatically and implemented them as unverified OCaml code. We used Coq’s extraction functionality to obtain an executable OCaml code of the reasoner.
Completeness proof was more challenging to mechanize than soundness proof. It required us to define a new invariant, fix errors in the original proof, and employ non-constructive reasoning.
Point 2 of Claim 1 in the original completeness proof involved a property that holds for the ifnal classification but does not necessarily hold in every intermediate step. To mechanize the proof, we defined a tree structure that encodes possible sequences of rule applications that lead to the current state. This structure allowed us to mimic doing induction over selected rule applications by doing induction over the trees. 5.1. Errors in Completeness Proofs Our mechanization revealed two major errors in pen-and-paper completeness proofs. The ifrst one is the non-transitivity of a relation assumed to be transitive. The second one is the under-specification of a solution for concrete domain predicates. We explain each problem and our solutions below.
Completeness proofs in Baader et. al. heavily rely on a relation defined with respect to a concept name denoted by ∼ . During our formalization, we discovered that ∼ is not transitive. The problem stemmed from the fact that in some models of the knowledge base, the interpretation of can be empty. We fixed this error by introducing -extensions to the algorithm that enforce nonemptiness while preserving subsumption. A-extension adds {} ⊑ ∃ . constraint to the CBox, where and are fresh individual and role names, respectively.
We identified another error in the statement of a lemma, originally called Claim 2, used in constructing a counterexample model. Original lemma states that “For each concrete domain and ∼ equivalence class, there exists a solution such that [...]”. However, this was too weak to imply the desired properties. We fixed this error by reordering the quantification to “For each ∼ equivalence class, there exists a solution such that, for each concrete domain [...]” and further restricting the behavior of the solution to the feature names that appear in the classification of the equivalence class.
We evaluated our work in two axes. We measured the required proof efort by comparing the number of lines of proof per line of implementation. Our 165 definitions consist of 1511 cloc. Our 387 theorems consist of 16977 cloc, giving us 11.3x proof overhead.
To evaluate the performance of our implementation, we measured run times on randomly generated knowledge bases with fixed set of names. For concept inclusion tests, we kept the number of role inclusion axioms at 10, and for role inclusion tests, we set the number of concept inclusions to 20. Our algorithm’s runtimes are 4s for 20, 278s for 30, and 192s for 40 concept inclusions; and 463s for 20, 6s for 30, and 2732s for 40 role inclusions. Our results indicates that the structure of a knowledge base more impactful on the performance than its size. We could not test our performance against the existing reasoners since interfacing with OWL is not implemented yet.
The Semantic Web, over the past three decades, helped enhance a wide range of applications. However, the varying sophistication of SW systems’ reasoning abilities highlights the need for reliable reasoning algorithms, particularly in the context of the growing interest in Neurosymbolic AI and Generative AI approaches that seek to utilize Semantic Web layers.
In an attempt to address this gap, our work lays the foundation for formally verified reasoners for Neurosymbolic AI applications. We believe that, in the cases of high-stakes application domains, such as health, finance, and security, the benefit of increased trustworthiness outweighs the increased development efort.
As future work, we are planning to integrate our reasoner into Protègè ontology editor [18] by creating a plugin to provide access to our reasoner for community use. We believe that having an easy access to verified reasoners will contribute to the adoption of formal methods in trustworthy AI. The second direction we will explore is reducing the trusted computing base by implementing a verified parser that will convert an OWL file to a VEL knowledge base. [18] M. A. Musen, The protégé project: a look back and a look forward, AI Matters 1 (2015) 4–12. URL: https://doi.org/10.1145/2757001.2757003. doi:10.1145/2757001.2757003.