Partially Finite Model Reasoning in Description Logics

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.