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

Speaker(s)

Tomasz Gogacz

Affiliation

Uniwersytet Warszawski

Date

Nov. 22, 2017, 2:15 p.m.

Room

room 5050

Seminar

Seminar Automata Theory

---

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.

---