Résumé | In this talk, we present logical formalisms in which reasoning about concrete domains is embedded in formulae at the atomic level. These mainly include temporal logics with concrete domains and description logics with concrete domains.
For the simple concrete domain (N,<), we present known proof techniques to handle satisfiable (infinite) symbolic models, sometimes at the cost of going beyond $omega$-regularity.
The talk is freely inspired from the paper "Concrete domains in logics: a survey" (2021) written with Karin Quaas (Leipzig University). |