Pith. sign in

REVIEW 3 major objections 4 minor 2 cited by

VEL: A Formally Verified Reasoner for OWL2 EL Profile

T0 review · 3 major / 4 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper establishes that VEL, a formally verified EL++ reasoner, is sound and complete for every input, with the proof machine-checked and executable OCaml code extracted from it.

desk verdict Solid formalization work with real proof fixes, but the end-to-end guarantee is oversold and the missing artifact makes the machine-checked claims unverifiable. read the letter →

arxiv 2412.08739 v1 pith:6HW3M4QY submitted 2024-12-11 cs.LO cs.AIcs.PL

Atalay Mert Ileri , Nalen Rangarajan , Jack Cannell , Hande McGinty This is my paper · ORCID
classification cs.LOcs.AIcs.PL
keywords formalverificationdescriptionlogicEL++OWL2ELprofilesubsumptioncheckingconcretedomainsproofextractionmachine-checkedproofs
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

VEL is a reasoner for the EL++ description logic that underlies the OWL2 EL profile, and its central claim is that the reasoner's subsumption answers are guaranteed correct for every possible input. Subsumption here means the question of whether one concept is logically forced to be a subclass of another under the ontology. The authors prove this guarantee with machine-checked proofs and then extract executable OCaml code from the verified definitions, so the guarantee is carried by the code itself rather than by any test suite. The proof effort also found two real errors in the published completeness proof of the base algorithm, which the authors repaired by changing the algorithm.

What carries the argument

The load-bearing objects are the normalized CBox and the classification records $S$ and $R$: $S$ maps each concept description to the concept descriptions it subsumes, and $R$ maps each role to the pairs of concept descriptions it relates. The repaired algorithm runs transformation, normalization, A-extension, and classification before checking whether $B$ (or $\bot$) appears in $S(A)$. A-extension adds a fresh individual $t$ and role $r_t$ with the axiom $\{t\} \sqsubseteq \exists r_t.A$, forcing $A$ to be nonempty in every model and restoring transitivity of the $\sim$ relation. The completeness proof is carried by role trees, an inductive structure recording how a pair $(C,D)$ entered $R(r)$ through the rules CR3, CR10, and CR11, which lets the proof maintain an invariant at every classification step instead of inducting over groups of rule applications.

What would settle it

Run the extracted reasoner on a knowledge base whose rational-number constraints force arithmetic beyond a 64-bit integer, or where the external solver's answer differs from the mathematical satisfiability of the constraint conjunction; a wrong subsumption verdict would refute the end-to-end guarantee for the runnable code.

Watch

Extended reading notes

Core claim

The central result is Theorem 2: for every knowledge base $\mathcal{C}$ and concept descriptions $C,D$, $\texttt{check\_subsumption}(\mathcal{C},C,D)=\texttt{true}$ exactly when $C \sqsubseteq_{\mathcal{C}} D$. Soundness and completeness are proved inside an interactive proof assistant for the full pipeline, namely transformation, normalization, A-extension, classification, and the final subsumption test, and the verified functions are extracted into runnable OCaml. Mechanizing the published completeness argument exposed two defects in it: the $\sim$ relation on reachable concept descriptions is not transitive in models where the queried concept $A$ has an empty extension, and the lemma that builds counterexample solutions for concrete-domain predicates was underspecified. The paper's fixes are an A-extension preprocessing step that forces $A$'s extension to be nonempty in all models, a modified normalization rule NF2, and a strengthened solution-existence lemma, with the remaining trust in the unverified concrete-domain checkers made explicit.

Load-bearing premise

The end-to-end guarantee is only as strong as the separately written, unverified programs that decide satisfiability and implication for rational-number and string constraints, plus the assumption that numbers never exceed 64-bit computer integers.

Editorial extensions

If this is right

  • The extracted OCaml reasoner's subsumption answers come with a static, machine-checked guarantee: no input can make it return a wrong answer, modulo the stated trusted computing base.
  • The two corrections, A-extension and the strengthened concrete-domain lemma, are necessary parts of the verified algorithm; the paper leaves open whether the original unmodified algorithm is complete.
  • The formalization provides a reusable semantic foundation for EL++ that other verified reasoners or ontology tooling can build on.
  • Because correctness is proved statically, the reasoner avoids runtime proof-certificate generation and checking, unlike validation-based approaches.
  • The supported concrete domains, rational numbers and strings, make the verified core usable on ontology queries that involve datatypes, at the price of trusting the unverified domain checkers.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper, the A-extension device suggests a general recipe for repairing completeness proofs that implicitly need some concept to be nonempty: add a fresh nominal and role that force nonemptiness at the classification level.
  • Beyond the paper, the unverified concrete-domain checkers are the most promising boundary to attack next; replacing them with verified or proof-producing satisfiability procedures would make the end-to-end claim fully closed.
  • Beyond the paper, the role-tree invariant is a transferable technique for mechanizing completeness proofs that originally require induction over selected rule applications rather than single steps.
  • Beyond the paper, one could benchmark VEL against production EL reasoners after swapping the functional $S$ and $R$ representation for persistent maps, since the paper identifies the lookup overhead as the main performance cost.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper presents VEL, a Coq formalization of a subsumption checker for the EL++ description logic, following the algorithm of Baader, Brandt, and Lutz. The formalization covers the EL++ language, semantics, normalization, a newly introduced A-extension step, and classification, and it culminates in Theorem 2, a Coq statement that the checker function is sound and complete with respect to EL++ subsumption. The authors extract OCaml code from the Coq development, add rational-number and string concrete domains backed by GLPK and OCamlgraph, and argue that the machine-checked proofs ensure correctness of the reasoner's outputs for all inputs. They also report discovering two errors in the original completeness proof, which motivate the A-extension and a strengthened concrete-domain solution lemma.

Significance. If the Coq development is as described, this would be a substantial contribution to verified reasoning: it mechanizes the semantics of EL++, provides a machine-checked proof of a nontrivial classification algorithm, identifies genuine gaps in a well-known pen-and-paper proof, and introduces reusable proof techniques such as role trees. The A-extension and the strengthened solution-existence lemma are concrete, falsifiable improvements over the original completeness argument. The paper also demonstrates a working extraction pipeline with two concrete domains. However, the advertised end-to-end guarantee for runnable outputs currently rests on unverified components and an acknowledged overflow risk, so the significance of the work as a verified reasoner depends on the authors closing or precisely qualifying that gap.

major comments (3)
  1. [String and Rational Number Domains / Trusted Computing Base] The paper states that satisfiability and implication checks for concrete domains are delegated to an unverified OCaml program using GLPK and OCamlgraph, and the Trusted Computing Base section lists these as trusted. This means Theorem 2, which is proved for the Coq function check_subsumption, does not by itself establish correctness of the extracted reasoner. If the unverified checker returns a wrong answer, the runnable code can contradict Theorem 2. The authors should make explicit how the Coq formalization interfaces with these unverified calls (e.g., as axioms or assumed specifications), and should either prove the checkers correct or clearly state that the end-to-end guarantee applies only to the Coq function, not the extracted executable.
  2. [Extraction] The Extraction section acknowledges that extracting Coq naturals and integers to 64-bit OCaml ints introduces possible overflow unsoundness. Since Theorem 2 quantifies over all inputs and the abstract claims "validity of outputs across all possible inputs," the extracted code does not meet that claim. The authors should either use Coq's default extraction to unbounded integers, or restrict the correctness statement to inputs and intermediate values that fit in 64 bits, with a clear statement that the extracted program is not guaranteed to be sound on all inputs.
  3. [General (artifact availability)] No artifact, repository link, or commit hash is provided, so the reader cannot inspect the Coq definitions, the proof scripts, or the extraction setup. For a formal-verification paper, the machine-checked proofs are the main evidence, and a named version of the development is essential for reproducibility. The authors should make the Coq development and the extracted OCaml code available and reference a specific commit or version in the paper.
minor comments (4)
  1. [Listing 2] The function signature in Listing 2 appears to contain a typo: check_subsumption(C, C, D) uses C twice, likely intending check_subsumption(C, C, D) with distinct arguments; this should be corrected for clarity.
  2. [Evaluation] The performance table shows highly non-monotonic runtimes (e.g., concept inclusions go from 4s at 20 constraints to 278s at 30 constraints and 192s at 40 constraints), with no error bars, number of runs, or explanation of variance. If the evaluation is meant to support scalability claims, it needs a more systematic methodology; otherwise it should be presented as anecdotal.
  3. [Evaluation] The proof-effort numbers (165 definitions, 387 theorems, 11.3x proof overhead) are useful, but the paper does not state which version of Coq or which library dependencies (other than mlvoqc) were used; this information should be added for reproducibility.
  4. [Trusted Computing Base] The Trusted Computing Base lists "OCaml run-time and libraries" and GLPK, but it does not mention the extraction mechanism itself or the axioms used for the concrete-domain checkers; the TCB should be stated in terms of the logical assumptions and the code-generation trust boundary.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the Coq proof is a self-contained derivation; unverified GLPK/OCamlgraph components and 64-bit extraction are explicit trust assumptions, not circular steps.

full rationale

The paper's central derivation is a Coq mechanization of Baader et al.'s EL++ classification algorithm. The soundness proof is by rule-invariance, and the completeness proof is repaired by two explicit, proved devices: A-extension (Theorem 1 is proved, not assumed) and role-tree invariants that track R-additions inductively. Neither device is a fitted input renamed as a prediction; each is a proof-level construction whose equivalence to the original semantics is established by theorem statements and proofs. The concrete-domain satisfiability and implication checkers are delegated to an unverified OCaml program using GLPK and OCamlgraph; this is listed in the Trusted Computing Base and is an external trust assumption, not a circular step. The Extraction section explicitly warns that mapping unbounded Coq naturals and integers to 64-bit OCaml ints can overflow, and it acknowledges this as a possible unsoundness; again, this is a gap between the Coq theorem and the runnable artifact, not a derivation of the conclusion from itself. Self-citations such as McGinty (2018) occur only in related-work context and are not load-bearing for the correctness claim. No quoted equation reduces to its own input, no fitted parameter is renamed as a prediction, and no uniqueness theorem from the authors' prior work is invoked to force the algorithm. The derivation chain is therefore self-contained apart from explicitly trusted external components, which is a trust boundary rather than circularity. The circularity score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The central correctness theorem relies on the standard trust in Coq plus the paper-specific assumptions that the unverified concrete-domain solvers are correct and that native int extraction does not overflow. There are no fitted free parameters and no invented entities.

assumptions (4)
  • standard math Soundness of the Coq proof assistant and correctness of its extraction mechanism for the used features.
    Trusted Computing Base section lists Coq and OCaml runtime as trusted; the theorem is only as strong as this foundation.
  • domain assumption Correctness of unverified OCaml concrete-domain satisfiability and implication checkers, including GLPK and OCamlgraph.
    The end-to-end correctness for all inputs depends on these oracles because they are not verified; paper states this in the Trusted Computing Base section.
  • ad hoc to paper Extraction from Coq's unbounded integers and naturals to native OCaml int does not overflow on the inputs encountered.
    The Extraction section admits this choice 'introduces possible unsoundness'; it is load-bearing for the runnable executable.
  • standard math Classical (non-constructive) reasoning principles used in the completeness proof are available and consistent.
    The paper notes the completeness proof 'employ[s] non-constructive reasoning'; in Coq this typically relies on classical axioms rather than pure CIC.

how reviews work

0 comments
Cite this review

Pith. "Pith review of VEL: A Formally Verified Reasoner for OWL2 EL Profile." pith.science (2026). https://pith.science/paper/6HW3M4QY

@misc{pith2026241208739,
  author       = {Pith},
  title        = {Pith review of: VEL: A Formally Verified Reasoner for OWL2 EL Profile},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6HW3M4QY}},
  note         = {Machine review of arXiv:2412.08739}
}
read the original abstract

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 recent 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 paper, we have developed VEL, a formally verified EL++ 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., has been transformed into executable OCaml code using the Coq proof assistant's extraction capabilities. Our formalization revealed several errors in the original completeness proofs, which led to changes to the algorithm to ensure its completeness. Our work demonstrates the necessity of mechanization of reasoning algorithms to ensure their correctness at theoretical and implementation levels.

Figures

Figures reproduced from arXiv: 2412.08739 by the authors.

Figure 1
Figure 1. Structure of VEL Implementation Our implementation of the reasoner consists of four parts: transformation, normalization, A-extension, and classifica￾tion. Transformation changes the problem from checking the subsumption of arbitrary concept descriptions to check￾ing the subsumption of two concept names. Normalization breaks down complex constraints into simpler ones to make subsumption checking tractable. A-extensi… view at source ↗
Figure 2
Figure 2. Example CBox where ∼ is not transitive. Role trees allowed us to mimic doing induction over se￾lected rule applications by doing induction over the trees. Although we didn’t need to use this technique again, we be￾lieve it is a strong technique to tackle proofs about properties that can be broken temporarily. Errors in Completeness Proofs Our mechanization revealed two major errors in pen￾and-paper completeness proo… view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Moose: Latent concept learning with reasoning-shortcut awareness in $\mathcal{EL}^{++}$

    cs.AI 2026-08 conditional novelty 7.0 of 10 partial

    Moose compiles OWL 2 EL ontologies into a Lean-verified differentiable weighted-model-counting layer and uses it to learn latent concept labels under partial supervision, beating propositional neuro-symbolic baselines...

  2. Charting the Future of Scholarly Knowledge with AI: A Community Perspective

    cs.DL 2025-08 unverdicted novelty 2.0 of 10

    A community perspective on how AI can support scholarly knowledge extraction, organization, and communication, with a proposed classification and ethical considerations.

Reference graph

Works this paper leans on

34 extracted references · 32 canonical work pages · cited by 2 Pith papers

  1. [1]

    Baader, F.; Brandt, S.; and Lutz, C. 2005. Pushing the EL Envelope. In Proceedings of the 19th International Joint Conference on Artificial Intelligence, IJCAI'05, 364–369. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc

    work page 2005

  2. [2]

    Baader , F.; Brandt , S.; and Lutz , C. 2008. Pushing the EL Envelope Further. In Clark , K.; and Patel-Schneider , P. F., eds., In Proceedings of the OWLED 2008 DC Workshop on OWL: Experiences and Directions

    work page 2008

  3. [3]

    Baader, F.; Koopmann, P.; and Tinelli, C. 2020. First Results on How to Certify Subsumptions Computed by the EL Reasoner ELK Using the Logical Framework with Side Conditions. Description Logics

    work page 2020

  4. [4]

    Al. I. Cuza University

    Bereczky, P.; Chen, X.; Horp \' a csi, D.; Mizsei, T. B.; Pe \ n a, L.; and Tusil, J. 2022. Mechanizing Matching Logic in Coq. In Rusu, V., ed., Proceedings of the Sixth Working Formal Methods Symposium, FROM 2022, "Al. I. Cuza University", Iasi, Romania, 19-20 September, 2022 , volume 369 of EPTCS , 17--36

    work page 2022

  5. [5]

    Bischof, S.; Schenner, G.; Steyskal, S.; and Taupe, R. 2018. Integrating Semantic Web Technologies and ASP for Product Configuration. In ConfWS, 53--60

    work page 2018

  6. [6]

    M.; and Di Sciascio, E

    Colucci, S.; Donini, F. M.; and Di Sciascio, E. 2024. A review of reasoning characteristics of RDF-based Semantic Web systems. Wiley Interdisciplinary Reviews: Data Mining and Knowledge Discovery, e1537

    work page 2024

  7. [7]

    de Almeida Borges, A. 2022. Towards a Coq formalization of a quantified modal logic. arXiv:2206.03358

    work page Pith review arXiv 2022

  8. [8]

    Free Software Foundation . 2024. GNU Linear Programming Kit

    work page 2024

Show all 34 references
  1. [9]

    Frumin, D. 2022. Semantic cut elimination for the logic of bunched implications, formalized in Coq. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022, 291–306. New York, NY, USA: Association for Computing Machinery. ISBN...

    2022

  2. [10]

    Glimm, B.; Horrocks, I.; Motik, B.; Stoilos, G.; and Wang, Z. 2014. HermiT: an OWL 2 reasoner. Journal of automated reasoning, 53: 245--269

    2014

  3. [11]

    Guo, D.; and Yu, W. 2023. A Comprehensive Formalization of Propositional Logic in Coq: Deduction Systems, Meta-Theorems, and Automation Tactics. Mathematics, 11(11)

    2023

  4. [12]

    Herbelin, H.; Kim, S.; and Lee, G. 2017. Formalizing the meta-theory of first-order predicate logic. Journal of the korean Mathematical society, 54(5): 1521--1536

    2017

  5. [13]

    J.; Alonso-Jim\' e nez, J

    Hidalgo-Doblado, M. J.; Alonso-Jim\' e nez, J. A.; Borrego-D\' az, J.; Mart\' n-Mateos, F. J.; and Ruiz-Reina, J. L. 2014. Formally Verified Tableau-Based Reasoners for a Description Logic. J. Autom. Reason., 52(3): 331–360

    2014

  6. [14]

    Hietala, K.; Rand, R.; Hung, S.-H.; Wu, X.; and Hicks, M. 2021. A verified optimizer for Quantum circuits. Proc. ACM Program. Lang., 5(POPL)

    2021

  7. [15]

    K.; and Zhou, L

    Hitzler, P.; Eberhart, A.; Ebrahimi, M.; Sarker, M. K.; and Zhou, L. 2022. Neuro-symbolic approaches in artificial intelligence . National Science Review, 9(6): nwac035

    2022

  8. [16]

    Jung, R.; Krebbers, R.; Jourdan, J.-H.; Bizjak, A.; Birkedal, L.; and Dreyer, D. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28: e20

    2018

  9. [17]

    Kazakov, Y.; Kr \"o tzsch, M.; and Simancik, F. 2012. ELK reasoner: architecture and evaluation. In ORE. Citeseer

    2012

  10. [18]

    Lutz, C. 2002. PSpace Reasoning with the Description Logic ALCF(D) . Logic Journal of the IGPL, 10(5): 535--568

    2002

  11. [19]

    Lutz, C. 2004. NEXP TIME-complete description logics with concrete domains. ACM Trans. Comput. Logic, 5(4): 669–705

    2004

  12. [20]

    McGinty, H. K. 2018. KNowledge Acquisition and Representation Methodology (KNARM) and Its Applications. Ph.D. thesis, University of Miami

    2018

  13. [21]

    B.; and Kumar, S

    Mishra, R. B.; and Kumar, S. 2011. Semantic web reasoners and languages. Artificial Intelligence Review, 35: 339--368

    2011

  14. [22]

    Musen, M. A. 2015. The prot \'e g \'e project: a look back and a look forward. AI matters, 1(4): 4--12

    2015

  15. [23]

    Necula, S.-C.; P a v a loaia, V.-D.; Str \^ mbei, C.; and Dospinescu, O. 2018. Enhancement of e-commerce websites with semantic web technologies. Sustainability, 10(6): 1955

    2018

  16. [24]

    S.; Glimm, B.; and Steigmiller, A

    Parsia, B.; Matentzoglu, N.; Gonçalves, R. S.; Glimm, B.; and Steigmiller, A. 2017. The OWL Reasoner Evaluation (ORE) 2015 Competition Report. Journal of Automated Reasoning, 59: 455 -- 482

    2017

  17. [25]

    Perera, M. 2020. Personalised human device interaction through context aware augmented reality. In Proceedings of the 2020 International Conference on Multimodal Interaction, 723--727

    2020

  18. [26]

    C.; Kalyanpur, A.; and Katz, Y

    Sirin, E.; Parsia, B.; Grau, B. C.; Kalyanpur, A.; and Katz, Y. 2007. Pellet: A practical owl-dl reasoner. Journal of Web Semantics, 5(2): 51--53

    2007

  19. [27]

    Smith, B.; Ashburner, M.; Rosse, C.; Bard, J. B. L.; Bug, W. J.; Ceusters, W.; Goldberg, L. J.; Eilbeck, K.; Ireland, A.; Mungall, C. J.; Leontis, N. B.; Rocca-Serra, P.; Ruttenberg, A.; Sansone, S.-A.; Scheuermann, R. H.; Shah, N. H.; Whetzel, P. L.; and Lewis, S. E. 2007. Th...

    2007

  20. [28]

    Steigmiller, A.; Liebig, T.; and Glimm, B. 2014. Konclude: system description. Journal of Web Semantics, 27: 78--85

    2014

  21. [29]

    The Coq Development Team . 2024. The Coq Proof Assistant, version 8.19.2

    2024

  22. [30]

    Tsarkov, D.; and Horrocks, I. 2006. FaCT++ description logic reasoner: System description. In International joint conference on automated reasoning, 292--297. Springer

    2006

  23. [31]

    Xavier, B.; Olarte, C.; Reis, G.; and Nigam, V. 2018. Mechanizing Focused Linear Logic in Coq. Electronic Notes in Theoretical Computer Science, 338: 219--236. The 12th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2017)

    2018

  24. [32]

    Zanarini, D.; Luna, C.; and Sierra, L. 2012. Alternating-Time Temporal Logic in the Calculus of (Co)Inductive Constructions. In Gheyi, R.; and Naumann, D., eds., Formal Methods: Foundations and Applications, 210--225. Berlin, Heidelberg: Springer Berlin Heidelberg. ISBN 978-3-...

    2012

  25. [33]

    , " * write output.state after.block = add.period write newline

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint howpublished institution isbn journal key month note number organization pages publisher school series title type volume year label extra.label sort.label short.list INTEGERS output.state before.all...

  26. [34]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.