Partially Finite Model Reasoning in Description Logics Extended Version

TL;DR

This paper introduces the concept of partially finite models in description logics, analyzing query entailment where part of the model must be finite, and provides complexity results for this reasoning task.

Contribution

It extends finite and infinite model reasoning to partially finite models in DLs, with complexity analysis and applications to query containment.

Findings

Partially finite query entailment in DL S is 2-EXPTIME-complete.

The approach involves sophisticated infinite model surgery techniques.

Application to query containment with closed predicates via reduction.

Abstract

Aiming to harmonise finite and infinite model reasoning, we initiate the study of partially finite models, where the reasoning task comes with a formula that specifies a part of the model that must be finite. We focus on the problem of partially finite query entailment in description logics (DLs): given a knowledge base (KB), a query, and a distinguished concept, decide whether the query holds in all models of the KB that interpret the distinguished concept as a finite set. To break the ground, we work with the DL S, an extension of the basic DL ALC with transitive roles, which is one of the simplest cases where finite and infinite query entailment diverge. Generalising previous results on the finite and infinite cases, we show that also partially finite entailment of conjunctive queries is in 2-exptime for S. The solution involves sophisticated infinite model surgery and goes far beyond combining the arguments for the two special cases. As a direct application, we show how the problem of query containment in the presence of closed predicates can be solved by reduction to partially finite query entailment.