Knowledge Representation (KR) formalisms provide precise specifications of algorithmic structure, yet it remains unclear whether gradient-trained neural networks implement these specifications even when they are theoretically expressible. Recent formal language theory tells us what Transformers can express—masked hard-attention Transformers recognize the star-free regular languages, equivalent to first-order logic with linear order (FO[<]) and linear temporal logic (LTL)—but not what gradient-trained Transformers will learn. We ask whether trained networks actually implement the logical circuits that theory predicts, and propose KR-Guided Mechanistic Verification to find out. The idea is to compile a B-RASP specification into a Structural Causal Model whose variables correspond to prescribed logical operations, then use Distributed Alignment Search to obtain quantitative, falsifiable causal evidence for or against each operation's presence in the trained network. We instantiate this framework on binary increment, a task for which B-RASP prescribes an explicit three-stage circuit implementable by a two-layer Transformer with O(poly(n)) parameters—exponentially fewer states than any fixed-precision recurrent or state space baselines require. The answer is affirmative: all three prescribed operations are faithfully encoded in dedicated neural subspaces, with wrong-specification controls at chance; Sparse Autoencoder decomposition independently recovers the same logical structure without supervision. Moreover, this structure is not acquired gradually: it emerges as a sharp phase transition during grokking, providing a specification-aligned progress measure that reveals what changes during the generalization transition, not merely that something changes. These results demonstrate that KR formalisms can serve not only as prescriptive specifications of what networks should compute, but as falsifiable causal hypotheses that mechanistic interpretability tools can rigorously test—bridging the gap between symbolic KR and neural computation.

Abstract Ontology matching (OM) plays an essential role in enabling semantic interoperability and integration across heterogeneous knowledge sources, particularly in biomedical domains which contain numerous complex concepts related to diseases and pharmaceuticals. This paper introduces GenOM , a large language model (LLM)-based ontology alignment framework, which enriches semantic representations of ontology concepts via generating textual definitions, retrieving alignment candidates with an embedding model, and incorporating exact lexical matching tools to improve precision. Extensive experiments conducted on the OAEI Bio-ML track demonstrate that GenOM can often achieve competitive performance, surpassing many baselines including traditional OM systems and recent LLM-based methods. Ablation studies confirm the effectiveness of semantic enrichment, highlighting the framework’s robustness and adaptability. Beyond the matching framework itself, this paper introduces a set of criteria for evaluating the quality of concept definitions that are generated, providing a more systematic basis for analysing LLM-generated descriptions.

Abstract Second-order quantifier-elimination is the problem of finding, given a formula with second-order quantifiers, a logically equivalent first-order formula. While such formulas are not computable in general, there are practical algorithms and subclasses with applications throughout computational logic. One of the most prominent algorithms for second-order quantifier elimination is the SCAN algorithm which is based on saturation theorem proving. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding an instance of the second-order quantifiers that results in a logically equivalent first-order formula. In addition we provide a prototype implementation of the proposed method. This work paves the way for applying the SCAN algorithm to new problems in application domains such as modal correspondence theory, knowledge representation, and verification.

Abstract In this paper, we present a practical method for computing uniform interpolation and forgetting in $$\mathcal {ELIH}$$ ELIH -ontologies, addressing fundamental operations critical for detecting semantic differences in ontology evolution. Our method extends previous work to accommodate inverse roles while maintaining soundness and termination guarantees. Empirical evaluation across industry benchmarks from Oxford ISG and NCBO BioPortal demonstrates 100% success rates with notable improvements in computational efficiency compared to state-of-the-art systems. The practical impact of our method has been validated through application to SNOMED CT, the world’s largest clinical terminology supporting healthcare information systems globally. This enables terminologists and developers to systematically track semantic differences, detect unintended consequences, and validate change safety across SNOMED CT releases.

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.

Abstract We investigate the systematic development of refined tableau systems for a subset of the logics of confluence, which are modal logics comprising of instances of the Scott-Lemmon axioms. In particular, we look at rule refinements aiming to decrease branching, perform fewer inferences and reduce the application of rules which create new labels in the tableau. Propagation rules are common forms of refined rules, that construct smaller pre-models sufficient to determine satisfiability, without needing to construct full concrete models satisfying the correspondence properties which would require a lot more inference steps. These rules have already been developed for the confluence logics that are part of the modal logic cube, but are lacking for some instances outside the cube. Such instances can be awkward, as the nature of their correspondence properties makes the development of propagation rules particularly challenging. These are the logics K G0111, K G and K De for which we propose refined tableau systems. We also present refined tableau systems for the combined logics K alt1De, K BG0111 and K DDe. Soundness and completeness results for all the systems are established.

Ontologies are being utilized widely as sources for formally organized information in a range of fields. The SNOMED CT ontology is a key resource in national and international health sectors for automatically linking information captured by diverse clinical information systems and research data ensuring consistent patient data capture and effective data analytics and decision support. Offering a comprehensive multilingual vocabulary for encoding clinical knowledge of multiple domains, the ontology is large and new releases are created regularly to reflect domain changes and user requirements. The main contribution of the paper is a novel automated approach for tracking semantic differences of subdomains in different versions of SNOMED CT targeted at terminologists, debuggers, ontology evaluators and developers of software using SNOMED CT. Whereas the semantic difference sets produced with existing methods are rather large and difficult to analyze, our method produces concise semantic difference sets for user-specified input focus concepts. Our method is based on subontology generation and semantic difference computation using uniform interpolation, which aids in finding inferred differences that other semantic difference tools do not reveal. The obtained semantic difference sets are related to the meaning of focus concept definitions for specific ontology subdomains, where some of these differences would not have been generated without this focused method for computing semantic differences between ontologies. A case study using SNOMED CT has shown the proposed approach is useful for domain experts.

Abstract Query answering is an important problem in AI, database and knowledge representation. In this paper, we develop saturation-based Boolean conjunctive query answering and rewriting procedures for the guarded, the loosely guarded and the clique-guarded fragments. Our query answering procedure improves existing resolution-based decision procedures for the guarded and the loosely guarded fragments and this procedure solves Boolean conjunctive query answering problems for the guarded, the loosely guarded and the clique-guarded fragments. Based on this query answering procedure, we also introduce a novel saturation-based query rewriting procedure for these guarded fragments. Unlike mainstream query answering and rewriting methods, our procedures derive a compact and reusable saturation, namely a closure of formulas, to handle the challenge of querying for distributed datasets. This paper lays the theoretical foundations for the first automated deduction decision procedures for Boolean conjunctive query answering and the first saturation-based Boolean conjunctive query rewriting in the guarded, the loosely guarded and the clique-guarded fragments.

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.

In this paper, we present a method for extracting subontologies from $\mathcalELH $ ontologies for a set of symbols. The approach is focused on the generation of upwardly abstracted definitions of concepts, which is a technique for computing definitions expressed using closest primitive ancestors. The subontologies returned by the method are evaluated for quality and compared to extracts computed with locality-based modularisation and uniform interpolation. Our subontology generation method produces promising results in terms of size and relevance to the needs of domain experts.

This paper investigates the problem of forgetting in description logics with nominals. In particular, we develop a practical method for forgetting concept and role names from ontologies specified in the description logic ALCO, extending the basic ALC with nominals. The method always terminates, and is sound in the sense that the forgetting solution computed by the method has the same logical consequences with the original ontology. The method is so far the only approach to deductive forgetting in description logics with nominals. An evaluation of a prototype implementation shows that the method achieves a significant speed-up and notably better success rates than the Lethe tool which performs deductive forgetting for ALC-ontologies. Compared to Fame, a semantic forgetting tool for ALCOIH-ontologies, better success rates are attained. From the perspective of ontology engineering this is very useful, as it provides ontology curators with a powerful tool to produce views of ontologies.

Signature-based abduction aims at building hypotheses over a specified set of names, the signature, that explain an observation relative to some background knowledge. This type of abduction is useful for tasks such as diagnosis, where the vocab- ulary used for observed symptoms differs from the vocabulary expected to explain those symptoms. We present the first complete method solving signature-based abduction for observations expressed in the expressive description logic ALC, which can include TBox and ABox axioms. The method is guaranteed to compute a finite and complete set of hypotheses, and is evaluated on a set of realistic knowledge bases.

Model generation is a problem complementary to theorem proving and is important for fault analysis and debugging of formal specifications of security protocols, programs and terminological definitions, for example. This paper discusses several ways of enhancing the paradigm of bottom-up model generation, with the two main contributions being a new range-restriction transformation and generalized blocking techniques. The range-restriction transformation refines existing transformations to range-restricted clauses by carefully limiting the creation of domain terms. The blocking techniques are based on simple transformations of the input set together with standard equality reasoning and redundancy elimination techniques, and allow for finding small, finite models. All possible combinations of the introduced techniques and a classical range-restriction technique were tested on the clausal problems of the TPTP Version 6.0.0 with an implementation based on the SPASS theorem prover using a hyperresolution-like refinement. Unrestricted domain blocking gave best results for satisfiable problems, showing that it is an indispensable technique for bottom-up model generation methods, that yields good results in combination with both new and classical range-restricting transformations. Limiting the creation of terms during the inference process by using the new range-restricting transformation has paid off, especially when using it together with a shifting transformation. The experimental results also show that classical range restriction with unrestricted blocking provides a useful complementary method. Overall, the results show bottom-up model generation methods are good for disproving theorems and generating models for satisfiable problems, but less efficient for unsatisfiable problems.

Abductive reasoning generates explanatory hypotheses for new observations using prior knowledge. This paper investigates the use of forgetting, also known as uniform interpolation, to perform ABox abduction in description logic (ALC) ontologies. Non-abducibles are specified by a forgetting signature which can contain concept, but not role, symbols. The resulting hypotheses are semantically minimal and consist of a disjunction of ABox axioms. These disjuncts are each independent explanations, and are not redundant with respect to the background ontology or the other disjuncts, representing a form of hypothesis space. The observations and hypotheses handled by the method can contain both atomic or complex ALC concepts, excluding role assertions, and are not restricted to Horn clauses. Two approaches to redundancy elimination are explored in practice: full and approximate. Using a prototype implementation, experiments were performed over a corpus of real world ontologies to investigate the practicality of both approaches across several settings.

This paper explores how the logical difference between two ontologies can be tracked using a forgetting-based or uniform interpolation (UI)-based approach. The idea is that rather than computing all entailments of one ontology not entailed by the other ontology, which would be computationally infeasible, only the strongest entailments not entailed in the other ontology are computed. To overcome drawbacks of existing forgetting/uniform interpolation tools we introduce a new forgetting method designed for the task of computing the logical difference between different versions of large-scale ontologies. The method is sound and terminating, and can compute uniform interpolants for ALC-ontologies as large as SNOMED CT and NCIt. Our evaluation shows that the method can achieve considerably better success rates (>90%) and provides a feasible approach to computing the logical difference in large-scale ontologies, as a case study on different versions of SNOMED CT and NCIt ontologies shows.

We are interested in the computation of ontology extracts based on forgetting from large ontologies in real-world scenarios. Such scenarios require nearly all of the terms in the ontology to be forgotten, which poses a significant challenge to forgetting tools. In this paper we show that modularization and forgetting can be combined beneficially in order to compute ontology extracts. While a module is a subset of axioms of a given ontology, the solution of forgetting (also known as a uniform interpolant) is a compact representation of the ontology limited to a subset of the signature. The approach introduced in this paper uses an iterative workflow of four stages: (i)~extension of the given signature and, if needed partitioning, (ii)~modularization, (iii)~forgetting, and (iv)~evaluation by domain expert. For modularization we use three kinds of modules: locality-based, semantic and minimal subsumption modules. For forgetting three tools are used: NUI, LETHE and FAME. An evaluation on the SNOMED CT and NCIt ontologies for standard concept name lists showed that precomputing ontology modules reduces the number of terms that need to be forgotten. An advantage of the presented approach is high precision of the computed ontology extracts.

Dependency quantified Boolean formulas (DQBF) and QBF dependency schemes have been treated separately in the literature, even though both treatments extend QBF by replacing the linear order of the quantifier prefix with a partial order. We propose to merge the two, by reinterpreting a dependency scheme as a mapping from QBF into DQBF. Our approach offers a fresh insight on the nature of soundness in proof systems for QBF with dependency schemes, in which a natural property called 'full exhibition' is central. We apply our approach to QBF proof systems from two distinct paradigms, termed 'universal reduction' and 'universal expansion'. We show that full exhibition is sufficient (but not necessary) for soundness in universal reduction systems for QBF with dependency schemes, whereas for expansion systems the same property characterises soundness exactly. We prove our results by investigating DQBF proof systems, and then employing our reinterpretation of dependency schemes. Finally, we show that the reflexive resolution path dependency scheme is fully exhibited, thereby proving a conjecture of Slivovsky.

This paper presents a practical method for computing solutions of concept forgetting in the description logic ALCOQ(neg,and,or), basic ALC extended with nominals, qualified number restrictions, role negation, role conjunction and role disjunction. The method is based on a non-trivial generalisation of Ackermann's Lemma, and attempts to compute either semantic solutions of concept forgetting or uniform interpolants in ALCOQ(neg,and,or). It is so far the only approach to concept forgetting in description logics with number restrictions plus nominals, as well as in description logics with ABoxes. Results of an evaluation with a prototypical implementation have shown that the method was successful in more than 90% of the test cases from a large corpus of biomedical ontologies. In only 13.2% of these cases the solutions were semantic solutions.

Forgetting refers to a non-standard reasoning problem concerned with eliminating concept and role symbols from description logic-based ontologies while preserving all logical consequences up to the remaining symbols. Whereas previous research has primarily focused on forgetting concept symbols, in this paper, we turn our attention to role symbol forgetting. In particular, we present a practical method for semantic role forgetting for ontologies expressible in the description logic ALCOQH(universal role), i.e., the basic description logic ALC extended with nominals, qualified number restrictions, role inclusions and the universal role. Being based on an Ackermann approach, the method is the only approach so far for forgetting role symbols in description logics with qualified number restrictions. The method is goal-oriented and incremental. It always terminates and is sound in the sense that the forgetting solution is equivalent to the original ontology up to the forgotten symbols possibly with new concept definer symbols. Despite our method not being complete, performance results of an evaluation with a prototypical implementation have shown very good success rates on real-world ontologies.

This paper investigates refinement techniques for semantic tableau calculi. The focus is on techniques to reduce branching in inference rules and thus allow more effective ways of carrying out deductions. We introduce an easy to apply, general principle of atomic rule refinement, which depends on a purely syntactic condition that can be easily verified. The refinement has a wide scope, for example, it is immediately applicable to inference rules associated with frame conditions of modal logics, or declarations of role properties in description logics, and it allows for routine development of hypertableau-like calculi for logics with disjunction and negation. The techniques are illustrated on Humberstone’s modal logic $${{\mathrm{K}_m}(\lnot )}$$ with modal operators defined with respect to both accessibility and inaccessibility, for which two refined calculi are given.

Uniform interpolation and the dual task of forgetting restrict the ontology to a specified subset of concept and role names. This makes them useful tools for ontology analysis, ontology evolution and information hiding. Most previous research focused on uniform interpolation of TBoxes. However, especially for applications in privacy and information hiding, it is essential that uniform interpolation methods can deal with ABoxes as well. We present the first method that can compute uniform interpolants of any ALC ontology with ABoxes. ABoxes bring their own challenges when computing uniform interpolants, possibly requiring disjunctive statements or nominals in the resulting ABox. Our method can compute representations of uniform interpolants in ALCO. An evaluation on realistic ontologies shows that these uniform interpolants can be practically computed, and can often even be presented in pure ALC.

This article presents a tableau approach for deciding expressive description logics with full role negation and role identity. We consider the description logic ALBO id , which is ALC extended with the Boolean role operators, inverse of roles, the identity role, and includes full support for individuals and singleton concepts. ALBO id is expressively equivalent to the two-variable fragment of first-order logic with equality and subsumes Boolean modal logic. In this article, we define a sound, complete, and terminating tableau calculus for ALBO id that provides the basis for decision procedures for this logic and all its sublogics. An important novelty of our approach is the use of a generic unrestricted blocking mechanism. Unrestricted blocking is based on equality reasoning and a conceptually simple rule, which performs case distinctions over the identity of individuals. The blocking mechanism ties the proof of termination of tableau derivations to the finite model property of ALBO id .

In this paper we present a translation principle, called the axiomatic translation , for reducing propositional modal logics with background theories, including triangular properties such as transitivity, Euclideanness and functionality, to decidable fragments of first-order logic. The goal of the axiomatic translation principle is to find simplified theories, which capture the inference problems in the original theory, but in a way that can be readily automated and is easier to deal with by existing (first-order) theorem provers than the standard translation. The principle of the axiomatic translation is conceptually very simple and can be almost completely automated. Soundness is automatic under reasonable assumptions, general decidability results can be stated and termination of ordered resolution is easily achieved. The non-trivial part of the approach is proving completeness. We prove results of completeness, decidability, model generation, the small model property and the interpolation property for a number of common and less common modal logics. We also present results of experiments with a number of first-order logic theorem provers which are very encouraging.

This paper proposes two methods for realising automated reasoning about agent-based systems. The framework for modelling intelligent agent behaviour that we focus on is a core of KARO logic, an expressive combination of various modal logics including propositional dynamic logic, a modal logic of knowledge, a modal logic of wishes, and additional non-standard operators. The first method we present is based on a translation of core KARO logic to first-order logic combined with first-order resolution. The second method uses an embedding of core KARO logic into a combination of branching-time temporal logic CTL and multi-modal S5 plus a clausal resolution calculus for these combined logics. We discuss the advantages and shortcomings of each approach and suggest ways to extend each variant to cover more of the KARO framework.

Normal modal logics can be defined axiomatically as Hilbert systems, or semantically in terms of Kripke's possible worlds and accessibility relations. Unfortunately there are Hilbert axioms which do not have corresponding first-order properties for the accessibility relation. For these logics the standard semantics-based theorem proving techniques, in particular, the relational translation into first-order predicate logic, do not work. There is an alternative translation, the so-called functional translation, in which the accessibility relations are replaced by certain terms which intuitively can be seen as functions mapping worlds to accessible worlds. In this paper we show that from a certain point of view this functional language is more expressive than the relational language, and that certain second-order frame properties can be mapped to first-order formulae expressed in the functional language. Moreover, we show how these formulae can be computed automatically from the Hilbert axioms. This extends the applicability of the functional translation method.

Abstract We present a two-sorted algebra, called a Peirce algebra , of relations and sets interacting with each other. In a Peirce algebra, sets can combine with each other as in a Boolean algebra, relations can combine with each other as in a relation algebra, and in addition we have both a set-forming operator on relations (the Peirce product of Boolean modules) and a relation-forming operator on sets (a cylindrification operation). Two applications of Peirce algebras are given. The first points out that Peirce algebras provide a natural algebraic framework for modelling certain programming constructs. The second shows that the so-called terminological logics arising in knowledge representation have evolved a semantics best described as a calculus of relations interacting with sets.