Exploring Non-Regular Extensions of Propositional Dynamic Logic with Description-Logics Features

Overview

• The paper investigates the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics that extend ALC.
• It focuses on two specific extensions: ALCreg, which is a variant of Propositional Dynamic Logic, and ALCvpl, which generalizes many known decidable non-regular extensions of ALCreg.
• The paper presents a series of undecidability results, including showing that the addition of the seemingly innocent Self operator leads to the loss of decidability for the concept satisfiability problem in ALCvpl, and that the concept satisfiability problem for ALCvpl extended with nominals is undecidable.
• Additionally, the paper establishes undecidability of query entailment for queries involving non-regular atoms, even in the case of ALC-TBoxes, which contrasts with the classical database setting.

Plain English Explanation

The paper explores how certain logical constructs, called "path expressions," can impact the decidability of satisfiability checking and querying in a family of description logics, which are a type of formal language used to represent and reason about knowledge.

Specifically, the researchers look at two extensions of a basic description logic called ALC: ALCreg, which is similar to a well-known logic called Propositional Dynamic Logic, and ALCvpl, which generalizes many previously known decidable extensions of ALCreg.

The key findings are:

• Adding a seemingly simple construct called the "Self" operator to ALCvpl causes the concept satisfiability problem (a fundamental reasoning task) to become undecidable, meaning there is no guaranteed way to determine if a given statement is true or false.
• The concept satisfiability problem for ALCvpl is also undecidable when extended with "nominals," which are a way to refer to specific individuals in the logic.
• Surprisingly, even for the simpler logic ALC, querying for certain non-regular patterns becomes undecidable, which is different from what happens in classical database settings.

These results highlight how seemingly minor additions to these logical formalisms can have significant impacts on their mathematical properties and reasoning capabilities.

Technical Explanation

The paper examines the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics that extend the basic logic ALC.

The authors focus on two specific extensions: ALCreg and ALCvpl. ALCreg is a notational variant of the well-known Propositional Dynamic Logic, while ALCvpl was introduced and investigated by Loding and Serre in 2007. ALCvpl generalizes many known decidable non-regular extensions of ALCreg.

The paper presents a series of undecidability results:

1. It is shown that the decidability of the concept satisfiability problem for ALCvpl is lost upon adding the seemingly innocent Self operator.
2. Undecidability is established for the concept satisfiability problem for ALCvpl extended with nominals (a way to refer to specific individuals). Interestingly, this undecidability proof relies on a single non-regular (visibly-pushdown) language, namely r#s# := { r^n s^n | n in N } for fixed role names r and s.
3. In contrast to the classical database setting, the paper establishes undecidability of query entailment for queries involving non-regular atoms from r#s#, already in the case of ALC-TBoxes (a type of knowledge base).

These results highlight the significant impact that seemingly minor additions to these logical formalisms can have on their mathematical properties and reasoning capabilities.

Critical Analysis

The paper presents a comprehensive analysis of the decidability issues that arise when incorporating non-regular path expressions, such as regular and visibly-pushdown languages, into description logics that extend ALC.

The key strength of the paper is the rigor of the undecidability proofs, which rely on carefully constructed examples and reductions to establish the loss of decidability for fundamental reasoning tasks like concept satisfiability and query entailment.

However, one potential limitation is that the paper does not explore the practical implications of these undecidability results. While the theoretical insights are valuable, it would be interesting to see a discussion of how these findings might impact the real-world application of description logics, particularly in areas like knowledge representation and reasoning.

Additionally, the paper does not delve into potential strategies for regaining decidability, such as by identifying restricted fragments or alternate language constructs that could preserve decidability. Exploring these avenues could provide valuable guidance for researchers and practitioners working with description logics.

Overall, the paper makes a significant contribution to the understanding of the interplay between non-regular path expressions and the decidability of description logics. The findings serve as an important cautionary tale, highlighting the care that must be taken when extending these logical formalisms to ensure their reasoning capabilities remain intact.

Conclusion

The paper investigates the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics that extend the basic logic ALC. The authors focus on two specific extensions: ALCreg and ALCvpl.

The key findings include the loss of decidability for the concept satisfiability problem in ALCvpl upon adding the Self operator, the undecidability of the concept satisfiability problem for ALCvpl extended with nominals, and the undecidability of query entailment for queries involving non-regular atoms, even in the case of ALC-TBoxes.

These results highlight the significant impact that seemingly minor additions to these logical formalisms can have on their mathematical properties and reasoning capabilities. The paper serves as an important contribution to the understanding of the interplay between non-regular path expressions and the decidability of description logics, providing valuable insights for researchers and practitioners working in this field.