Jakub Gajarský, Model Checking on Interpretations of Classes of Bounded Local Clique-Width
The first-order model checking problem for finite graphs asks, given a graph G and a first-order sentence $\phi$ as input, to decide whether $\phi$ holds on G. Showing the existence …