ABSTRACT. It is known that the problems of deciding the existence of Craig interpolants and of explicit definitions of concepts are both 2ExpTime-complete for standard description logics with nominals and/or role inclusions. These complexity results depend on the presence of an ontology. In this article, we first consider the case without ontologies (or, in the case of role inclusions, ontologies only containing role inclusions) and show that both the existence of Craig interpolants and of explicit definitions of concepts become coNExpTime-complete for DLs such as ALCO and ALCH. Secondly, we make a few observations regarding the size and computation of interpolants and explicit definitions, both with ontologies and without.

ABSTRACT. (This is an extended abstract on our paper accepted at ESWC 2022.)

ABSTRACT. Forgetting is an important ontology extraction technique. A variant of forgetting which has received significant attention in the literature is \emph{deductive forgetting}. While \emph{deductive forgetting} is attractive as it generates the forgetting view in a language with the same complexity as the language of the original ontology, it is known to be not precise as it may not preserve the information that requires more complex languages. We study \emph{deductive forgetting} with the aim of understanding the unpreserved information. We present a system that performs \emph{deductive forgetting} and produces a set of axioms~$\Delta$ representing the unpreserved information in the forgetting view. Our system allows a new fine-grained ontology extraction process that gives the user the option to enhance the informativeness of the deductive forgetting view by appending to it axioms from~$\Delta$.

ABSTRACT. We introduce a framework that allows for the construction of sequent systems for expressive description logics extending ALC. Our framework not only covers a wide array of common description logics, but also allows for sequent systems to be obtained for extensions of description logics with special formulae that we call role relational axioms. All sequent systems are sound, complete, and possess favorable properties such as height-preserving admissibility of common structural rules and height-preserving invertibility of rules.

ABSTRACT. Decidability of inferencing is commonly considered a very important property of logic-based knowledge representation formalisms, required for the algorithmization and automation of reasoning. Yet, oftentimes, the corresponding (un)decidability arguments are idiosyncratic and do not shed much light on the underlying principles governing the divide.

In my talk, I will review generic model- and proof-theoretic criteria for decidability of satisfiability and querying in fragments of first-order logic. Description logics play a central role in these considerations: On the one hand, they can serve as a simplified “testbed” inspiring decidability criteria which can then be generalized to higher arities. On the other hand, they mark a “sweet spot,” highlighting the fact that restricting to a binary setting allows for adding modeling features that would otherwise cause undecidability.

ABSTRACT. State constraints in AI Planning globally restrict the legal environment states. Standard planning languages make closed-domain and closed-world assumptions. Here we address open-world state constraints formalized by planning over a description logic (DL) ontology. Previously, this combination of DL and planning has been investigated for the light-weight DL DL-Lite. Here we propose a novel compilation scheme into standard PDDL with derived predicates, which applies to more expressive DLs and is based on the rewritability of DL queries into Datalog with stratified negation. We also provide a new rewritability result for the DL Horn-ALCHOIQ, which allows us to apply our compilation scheme to quite expressive ontologies. In contrast, we show that in the slight extension Horn-SROIQ no such compilation is possible unless the weak exponential hierarchy collapses. Finally, we show that our approach can outperform previous work on existing benchmarks for planning with DL ontologies, and is feasible on new benchmarks taking advantage of more expressive ontologies. It is an abstract of a paper accepted at AAAI-22.

ABSTRACT. We present two alternative algorithms for computing (all or some) solutions to the concept abduction problem: one algorithms is based on Reiter's hitting set tree algorithm, whereas the other on relies on a SAT encoding. In contrast to previous work, the algorithms do not rely on a refutation-based calculus and, hence, can be used also with efficient reasoners for tractable DLs such as EL and its extensions. An adaptation to other forms of (logic-based) abduction, e.g., to ABox abduction, is also possible.

ABSTRACT. When working with description logic ontologies, understanding entailments derived by a description logic reasoner is not always straightforward. So far, the standard ontology editor Protégé offers two services to help: (black-box) justifications for OWL 2 DL ontologies, and (glass-box) proofs for lightweight OWL EL ontologies, where the latter exploits the proof facilities of reasoner ELK. Since justifications are often insufficient in explaining inferences, there is thus only little tool support for explaining inferences in more expressive DLs. In this paper, we introduce EVEE-LIBS, a Java library for computing proofs for DLs up to ALCH, and EVEE-PROTEGE, a collection of Protégé plugins for displaying those proofs in Protégé. We also give a short glimpse of the latest version of EVONNE, a more advanced standalone application for displaying and interacting with proofs computed with EVEE-LIBS.

ABSTRACT. Propositional SAT solvers have been a popular way of computing justifications for ontological entailment -- minimal subsets of axioms of the ontologies that entail a given conclusion. Most SAT encodings proposed for Description Logics (DLs), translate the inferences obtained by a consequence-based procedure to propositional Horn clauses, using which entailments from subsets of axioms can be effectively checked, and use modified SAT solvers to systematically search over these subsets. To avoid repeated discovery of subsets with already checked entailment, the modified SAT solvers add special blocking clauses that prevent generating truth assignments corresponding to these subsets, the number of which can be exponential, even if the number of justifications is small. In this paper, we propose alternative SAT encodings that avoid generation of unnecessary blocking clauses. Unlike the previous methods, the inferences are used not only for checking entailment from subsets of axioms, but also, as a part of the encoding, to ensure that the SAT solver generates truth assignments corresponding only to justifications.

ABSTRACT. As abduction is getting more attention in the world of ontologies, multiple abduction solvers for DL have been developed. So far, however, there was no attempt for an unified API that would enable to integrate any DL abduction solver into an application – much in the spirit of the well known OWL API that is now implemented by most deductive DL reasoners. Abstracting the common functionality of multiple DL abduction solvers, we introduce DL Abduction API, that we hope can help to fill this space.

ABSTRACT. Weighted Threshold Operators are n-ary operators that compute a weighted sum of their arguments and verify whether it reaches a certain threshold. They have been extensively studied in the area of circuit complexity theory, as well as in the neural network community under the name of perceptrons. In Knowledge Representation, they have been introduced in the context of standard DL languages by adding a new constructor, the Tooth operator. Tooth-operators have been shown to behave like linear classification models. Thus, they can play a role in bridging symbolic and sub-symbolic reasoning approaches. In particular, tooth expressions can provide a powerful yet natural tool to represent local explanations of black-box classifiers in the context of Explainable AI. In this paper, we present the result of a user study in which we evaluated the interpretability of tooth expressions, and we compared them with Disjunctive Normal Forms (DNF). In the user study, we asked respondents with different backgrounds to perform distinct classification tasks using concepts represented either as tooth expressions or as different types of DNF formulas. We evaluated interpretability through accuracy, response time, confidence, and perceived understandability by human users. We expected tooth expressions to be generally more interpretable than DNFs. In line with our hypothesis, the study revealed that tooth expressions are generally faster to use, and that they are perceived more understandable by users who are less familiar with logic. Our study also showed that the type of task, the type of DNF, and the background of the respondents affect the interpretability of the formalism used.

ABSTRACT. In this paper we present a new labelled Natural Deduction calculus for the logic iALC, an intuitionistic description logic with nominals originally designed to reason over laws and other normative sentences in general. Even though this logic already has a formalised Sequent Calculus system, in practice Natural Deduction is more adequate in regards to making proofs more explainable - which is further aided by our use of labels. Finally, we prove soundness and normalisation for the new Natural Deduction system, and show its completeness.

ABSTRACT. The network control plane is a complex distributed system that runs various protocols for exchanging messages between routers and selecting paths for routing traffic. Errors in control plane configurations can lead to expensive outages or critical security breaches. The last decade has seen tremendous advances in applying formal methods to ensure their correctness.

In this talk, I will describe our logic-based approach that leverages Satisfiability Modulo Theory (SMT) solvers to verify a wide variety of network correctness properties including reachability, fault-tolerance, router equivalence, and load balancing. Although this approach is general and powerful, and works well for small-sized networks (with a few hundred routers), there are scalability challenges. I will then describe some recent improvements based on key abstractions and modular assume-guarantee reasoning that have enabled our SMT-based approach to successfully handle large-sized networks (with several thousands of routers), similar to those in operation in modern data centers.

This talk describes joint work with Ryan Beckett, Ratul Mahajan, Divya Raghunathan, Timothy Alberdingk Thijm, and David Walker.