The unification of neural learning and symbolic reasoning remains a foundational challenge in AI, forcing a persistent trade-off between logical rigor and computational scale. The field has largely diverged into two paths: expressive frameworks rooted in first-order logic that are formally sound but computationally intractable, and scalable methods, such as geometric embeddings, that sacrifice formal logical guarantees for efficiency. In this paper, we introduce DF-ɛℒ++, an end-to-end differentiable framework that transcends this trade-off by unifying PTIME-complete reasoning with neural learning. Our primary contribution is a complete, theoretically-grounded methodology centered on a unified semantic-loss framework: we unite the tractable structure of the Description Logic ɛℒ++ with a Product-based fuzzy semantics, deriving our learning objective directly from the corresponding Goguen implication to ensure high logical fidelity. This principled semantic core is made robust and practical by two supporting innovations: a normalization strategy that re-architects complex axioms for stable optimization, and a novel domain construction technique that prevents model collapse to ensure non-trivial reasoning. Validated on massive, real-world ontologies like SNOMED CT (377K concepts), DF-ɛℒ++ demonstrates a unique synergy of scale and performance: it remains computationally efficient where expressive systems fail, while decisively outperforming dominant scalable baselines in a range of knowledge base completion tasks with up to a 42% relative improvement in Hits@1. This work establishes a new, provably sound, and scalable pathway for a new generation of neuro-symbolic systems that are both empirically powerful and logically reliable.

Current neural biomedical entity linking (BioEL) models treat ontologies as flat dictionaries, ignoring the rich terminological knowledge (TBox) that defines concept boundaries. Consequently, they struggle with contextual ambiguity, often retrieving logically inconsistent candidates based solely on surface similarity. We present OntoEL, a neuro-symbolic framework that shifts BioEL from surface-level matching to logic-grounded reasoning. OntoEL integrates differentiable fuzzy EL⊥ reasoning into the retrieval pipeline as a consistency-aware re-ranker, employing a hybrid strategy: structural TBox reasoning is delegated to classical polynomial-time reasoners, while the sigmoidal Reichenbach implication performs soft type-consistency evaluation, effectively resolving the "implication bias" gradient pathology in previous neuro-symbolic methods. By enforcing ontological axioms as differentiable soft constraints, OntoEL aligns neural representations with logical truth. Comprehensive experiments on three benchmarks (MedMentions, BC5CDR, and NCBI Disease) demonstrate state-of-the-art performance, surpassing strong baselines by up to 4.2% in Accuracy@1. On highly ambiguous mentions requiring ontological reasoning, our method corrects 71.2% of retrieval errors, proving the efficacy of incorporating logical semantics into neural retrieval.

Forgetting is a non-standard reasoning procedure used to refine an ontology into a sub-signature by eliminating symbols not included in this subset, addressing fundamental challenges in knowledge management where ontology refinement and reuse are crucial for efficient information processing. It has two forms: weak forgetting (aka uniform interpolation), which preserves entailments within the source language, and strong forgetting, which additionally ensures model preservation modulo the eliminated symbols. This makes the latter significantly more challenging to compute. In this paper, we present the first method for strong role forgetting in description logics with qualified number restrictions (Q ). In particular, the method takes ALCQ-ontologies as input, yielding output either in ALCQ or in ALCQ(∇) by further incorporating the universal role ∇ to avoid information loss. This preserves model-theoretic properties crucial for applications such as modal correspondence theory and second-order quantifier elimination. While the method guarantees termination and soundness, its completeness is inherently constrained by the undecidability of strong forgetting. However, empirical evaluations on the Oxford-ISG and BioPortal benchmarks show that this theoretical limitation barely impedes practical utility, with experiment results demonstrating superb success rates and remarkably high efficiency.

Modern ontologies undergo continuous evolution to accommodate new domain knowledge, correct modeling errors, and adapt to changing user requirements. Monitoring these changes is crucial for maintaining ontology quality and understanding the semantic impact of modifications on dependent systems and applications. This paper describes OntoLDiff, a highly efficient system for tracking the logical difference between two ontologies formulated in the description logic ELH. Intuitively, the logical difference between two versions of an ontology refers to the set of axioms entailed by one version but not the other, indicating the information gain or loss between them. Typically, such axioms, referred to as 'witnesses ', can be infinite, making logical difference computation infeasible. To address this challenge, OntoLDiff employs a Uniform Interpolation (UI) approach to compute a finite representation of these axioms. Instead of computing all the entailments of one ontology but not the other, which would be computationally infeasible, the UI-based approach focuses on identifying only the strongest entailments, from which all witnesses can in principle be computed from its deductive closure. Despite UI's computational complexity, OntoLDiff is currently the only tool that efficiently tracks logical differences in industrial-scale ontologies, enabling ontology curators to precisely identify meaningful changes during ontology evolution.

Neuro-symbolic computing aims to integrate neural learning with symbolic reasoning to address the fundamental challenge of symbol grounding. While neural networks excel at pattern recognition, they struggle to maintain logical consistency. Conversely, symbolic systems provide formal reasoning capabilities but lack mechanisms for handling perceptual uncertainty. This paper introduces EmALC, a novel neuro-symbolic framework that bridges neural perception with symbolic logic through differentiable fuzzy semantics. Our approach addresses a key limitation of existing methods: while previous neuro-symbolic approaches like Logic Tensor Networks employ first-order fuzzy logic, where key reasoning problems are undecidable, EmALC ensures decidable reasoning by leveraging a fuzzy variant of ALC -- a decidable fragment of first-order logic. Unlike previous approaches that often compromise logical soundness for learning capability, EmALC maintains provable semantic consistency through a hierarchical loss function while mitigating reasoning shortcuts via rule-based revision strategies. Experimental evaluation demonstrates EmALC's effectiveness: on ontology revision tasks, it achieves 100% success rate in correcting masked groundings while preserving semantic integrity; on semantic image interpretation tasks, it improves object classification F1-scores by up to 5.56% through ontology-guided knowledge revision.

Uniform Interpolation (UI) is an advanced non-standard reasoning service that seeks to refine ontologies by creating rewritten modules. These modules, known as uniform interpolants, retain only "relevant names" while preserving their meanings in the absence of other names. UI holds significant potential across various domains where tailored ontology modules are required. However, realizing its full potential demands highly optimized techniques for generating such modules. Previous studies have identified notable challenges in generating uniform interpolants for EL-ontologies, where their computation is substantially more complex and computationally demanding than standard subset modules.

Uniform Interpolation (UI) is an advanced reasoning service used to narrow down an ontology to a restricted view. This new ontology, known as a uniform interpolant, will only consist of the ''relevant names'', yet it will retain their original meanings. UI is immensely promising due to its applicability across various domains where custom views of ontologies are essential. Nonetheless, to unlock its full potential, we need optimized techniques to generate these tailored views. Previous studies suggest that creating uniform interpolants for EL-ontologies is notably challenging. In some instances, it is not even feasible to compute a uniform interpolant; when feasible, the size of the uniform interpolant can be up to triple exponentially larger than the source ontology. Despite these challenges, our paper introduces an improved ''forgetting'' technique specifically designed for computing uniform interpolants of ELI-ontologies. We demonstrate that, with good normalization and inference strategies, such uniform interpolants can be efficiently computed, just as quickly as computing ''modules''. A comprehensive evaluation with a prototypical implementation of the method shows superb success rates over two popular benchmark datasets, demonstrating a clear computational advantage over state-of-the-art approaches.

Uniform interpolation (UI) is a non-standard reasoning service that seeks to project an ontology down to its sub-signature --- given an ontology taking a certain signature, and a subset Σ of "relevant names'' of that signature, compute a new ontology, called a uniform interpolant, that uses only the relevant names while preserving the semantics of the relevant names in the uniform interpolant. UI is of great potential importance since it may be used in a variety of applications where suitable views of ontologies need to be computed. However, this potential can only be fully realized if a highly optimized method for computing such views exists. Previous research has shown that computing uniform interpolants of ELH-ontologies is a computationally extremely hard problem --- a finite uniform interpolant does not always exist for ELH, and if it exists, then there exists one of at most triple exponential size in terms of the original ontology, and that, in the worst case, no shorter interpolant exists. Despite the inherent difficulty of the problem, in this paper, we present a highly optimized forgetting method for computing uniform interpolants of ELH-ontologies, and show however that, with good reduction and inference strategies, such uniform interpolants can be efficiently computed. The method is an improvement of the one presented in our previous work. What sets it apart is its flexibility to treat concept names of different types differently, effectively cutting down on the inferences involved. This treatment is primarily driven by the polarities of the concept names within an ontology. A comprehensive evaluation with a prototypical implementation of the method shows >95% average success rates over two popular benchmark datasets and demonstrates a clear computational advantage over state-of-the-art systems.

Developing ontologies for the Semantic Web is a time-consuming and error-prone task that typically requires the investment of considerable manpower and resources, as well as collaborative efforts. A potentially better idea is to reuse the “off-the-shelf” ontologies, whenever possible, somehow as per certain demands and requirements. A promising way to achieve ontology reuse is through creating views of ontologies, analogous to creating views of databases, with the resulting views focusing on specific topics and content of the original ontologies. This paper explores the problem of creating views of ontologies using a uniform interpolation approach. In particular, we develop a novel and practical uniform interpolation method for creating signature-based views for ontologies specified in the description logic , a very expressive description logic for which uniform interpolation has not been fully addressed. The method is terminating and sound, and computes uniform interpolants of -ontologies by eliminating from the input ontologies the names not used in the view using a forgetting procedure. This makes it the first and so far the only approach to eliminate both concept and (non-transitive) role names from -ontologies. Despite the inherent difficulty of uniform interpolation for this level of expressivity, an empirical evaluation with a prototypical implementation show very good success rates on a corpus of real-world ontologies, and demonstrates clear algorithmic advantage over the state-of-the-art system LETHE. This is extremely useful from the semantic web perspective, as it provides knowledge engineers with a powerful tool to create views of ontologies for ontology reuse.

This paper is concerned with the problem of computing the semantic difference between different versions of large-scale ontological knowledge bases using a uniform interpolation (UI) approach. The semantic difference between two versions of an ontology are the axioms entailed by one version but not the other version, reflecting the evolutionary changes of the content of the ontology. In general, computing such axioms is not computationally feasible, since there are infinitely many of them. UI is an advanced reasoning technique that seeks to create restricted views of ontologies; it provides an effective means for computing a finite representation of the difference between two ontologies. While existing UI methods are designed for languages that are either more expressive or less expressive than the description logic ELH, the underlying language of typical large-scale ontologies, in this paper, we introduce a practical UI method tailored for the task of computing the semantic difference in large-scale ELH-ontologies. The method is terminating, sound, and can always compute UI results possibly including fresh definer symbols. Two case studies on different versions of the SNOMED CT terminology show that the method has overcome major limitations of existing UI methods and can be used to reveal modeling changes that have occurred over successive releases of SNOMED CT.

This paper tackles the problem of computing views of OWL ontologies using a forgetting-based approach. In traditional relational databases, a view is a subset of a database, whereas in ontologies, a view is more than a subset; it contains not only axioms contained in the original ontology, but may also contain newly-derived axioms entailed by the original ontology (implicitly contained in the original ontology). Specifically, given an ontology , the signature of is the set of all the names in , and a view of is a new ontology obtained from using only part of ’s signature, namely the target signature, while preserving all logical entailments up to the target signature. Computing views of OWL ontologies is useful for Semantic Web applications such as ontology-based query answering, in a way that the view can be used as a substitute of the original ontology to answer queries formulated with the target signature, and information hiding, in the sense that it restricts users from viewing certain information of an ontology.

This paper describes a Java-based forgetting system UI-FAME for creating views of ontologies. In relational databases, a view is a subset of the database, while in ontologies, a view is more than a subset; it contains not only axioms that are contained in the original ontology, but also newly-derived axioms that are entailed by the original ontology. Forgetting is a form of non-standard reasoning that can be used to create views of ontologies by eliminating from the ontologies a set of concept and role names, namely the forgetting signature, while keeping all logical consequences over the names in the remaining signature. We compared UI-FAME with publicly accessible forgetting systems, namely LETHE and an early prototypical version of UI-FAME, over the 'AL'-TBox fragment of 494 ontologies taken from the Oxford Ontology Library. The results showed that UI-FAME had better success rates than LETHE and its prototypical version, and outsped LETHE by a large margin. UI-FAME has been integrated as back-end support in Babylon Health's (a leading digital healthcare company based in London) knowledge base (formed by the merger and alignment of medical ontologies from different sources) interfaces for their main concerns of ontology analysis and keeping track of the changes in different versions of its knowledge base.