Title: Combining Logical and Numerical Reasoning – Representation and Reasoning in Description Logics with Numbers

Duration: 2022 – 2025

Research Area: Mathematical Foundations and Statistical Learning

Description Logics (DLs) are a prominent family of symbolic AI formalisms that form the basis of the Web Ontology Language (OWL) and are used to specify and reason about ontologies in many application domains. However, classical DLs cannot directly express certain application-relevant numerical constraints. To overcome this deficit, different kinds of numerical extensions of DLs have been proposed in the literature, such as:

1. Description Logics with cardinality restrictions (which can, e.g., express a certain circuit gate having more inputs than outputs)
2. Description Logics with concrete domain restrictions (which can, e.g., represent the heart rate of a patient and compare it with a threshold value or other measurements)
3. Probabilistic extensions of Description Logics (which can, e.g., express the probability that a protein with a binding to a certain type of molecule possesses some characteristic of interest)

The aim of this project is to investigate the formal properties of such quantitative extensions of DLs and develop new mathematical tools that support such investigations.

Aims

This project has three main goals:

1. Develop mathematical tools for the analysis of the expressive power of the quantitative DLs and apply them to the three types of numerical extensions of DLs mentioned above.
2. Study the problem of model counting for ontologies written in such logics, and apply this.
3. Combine reasoners and algorithmic techniques for Description Logics and solvers from the area of Satisfiability Modulo Theories (SMT) to obtain more practical reasoners for quantitative DLs.

Problem

• Can we use known results from (finite) model theory to characterize the expressive power of Description Logics with cardinality constraints and concrete domain restrictions, as well as understand model counting in these languages? If not, what new notions and theories need to be developed?
• Can we design algorithms or combinations of reasoning systems that are suitable for the implementation and deployment of logical reasoners over ontologies containing expressive cardinality constraints or concrete domain restrictions?

Technology

Research focusing on goals (1) and (2) is of a theoretical nature and uses methods developed in mathematical logic, modal logic, and (finite) model theory. To address goal (3), we will combine methods developed in Knowledge Representation and Reasoning (e.g., tableau- and consequence-based reasoners) with methods developed in Automated Deduction and Formal Methods (e.g., SMT solvers) to obtain reasoners for quantitative DLs.

Outlook

This project will enhance both the understanding of formal properties of quantitative DLs and their usability in applications that require such DLs.

Publications

• Franz Baader and Filippo De Bortoli: The Abstract Expressive Power of First-Order and Description Logics with Concrete Domains. In The 39th ACM/SIGAPP Symposium on Applied Computing (SAC ’24), April 8–12, 2024, Avila, Spain. ACM, New York, NY, USA, Article 4, 8 pages. https://doi.org/10.1145/3605098.3635984 (To appear)
• Franz Baader and Filippo De Bortoli: On the Abstract Expressive Power of Description Logics with Concrete Domains. In Oliver Kutz and Ana Ozaki (eds.). Proceedings of the 36th International Workshop on Description Logics (DL’23), volume 3515 of CEUR Workshop Proceedings. Rhodes, Greece, CEUR-WS, 2023. https://ceur-ws.org/Vol-3515/paper-3.pdf
• Franz Baader, Jakub Rydval: Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains. J. Autom. Reason. 66(3): 357-407 (2022). https://doi.org/10.1007/s10817-022-09626-2

Team

Lead

• Prof. Dr.-Ing. Franz Baader

Team Members

• Dr. Anton Claußnitzer
• Filippo De Bortoli

Partners

• TUD Dresden University of Technology