Nominals, Inverses, Counting, and Conjunctive Queries or: Why Infinity is your Friend!

I will present a nice result in Knowledge Representation. It is a proof of decidability of query entailment for a certain extension of modal logic.
The procedure consists of two semi-recursive procedures. The first is standard: we try to derive proof of query treating it just as an FO formula.
The second one is tricky: They have shown that if query is not entailed, then there exists a finitely representable (not necessarily finite) counter model to the query. So we can enumerate all finitely representable structures.