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 proper minor-closed graph class, model-checking for FOL+DP can be done in quadratic time. We also introduce an extension of FOL+DP, namely the scattered disjoint paths logic, FOL+SDP, where we further consider the atomic predicate $s{\sf -sdp}_k(x_1,y_1,\ldots,x_k,y_k),$ demanding that the disjoint paths are within distance bigger than some fixed value $s$. Using the same technique we prove that model-checking for FOL+SDP can be done in quadratic time on classes of graphs with bounded Euler genus.

翻译：不交路径逻辑FOL+DP是一阶逻辑（FOL）的扩展，它额外包含原子谓词$\mathsf{dp}_k(x_1,y_1,\ldots,x_k,y_k)$，表示对于$i\in\{1,\ldots, k\}$，在$x_i$和$y_i$之间存在内部顶点不交路径。该逻辑能够表达大量超出FOL表达能力的难题。我们证明，对于每一个真极小闭图类，FOL+DP的模型检验可以在二次时间内完成。我们还引入了FOL+DP的一个扩展，即分散不交路径逻辑FOL+SDP，其中进一步考虑了原子谓词$s{\sf -sdp}_k(x_1,y_1,\ldots,x_k,y_k)$，要求不交路径之间的距离大于某个固定值$s$。运用相同技术，我们证明在具有有界欧拉亏格的图类上，FOL+SDP的模型检验可以在二次时间内完成。