Giannos Stamoulis, Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes
Giannos Stamoulis, Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes
The disjoint paths logic, FOL+DP, is an extension of First Order Logic (FOL) with the extra atomic predicate $\mathsf{dp}_k(x_1,y_1,\ldots,x_k,y_k),$ expressing the existence of internally vertex-disjoint paths between $x_i$ and $y_i,$ for $i\in \{1,\ldots, k\}$. This logic can express a wide variety of problems that escape the expressibility potential of FOL. We prove that for every …