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）是对一阶逻辑的扩展，新增了原子谓词$\mathsf{dp}_k(x_1,y_1,\ldots,x_k,y_k)$，用于表示存在内部顶点不相交的路径分别连接$x_i$和$y_i$（$i\in\{1,\ldots, k\}$）。该逻辑可表达一阶逻辑无法描述的各种问题。我们证明：对于所有真子图闭图类，FOL+DP的模型检验可在二次时间内完成。此外，我们引入FOL+DP的扩展——分散不相交路径逻辑（FOL+SDP），其中进一步考虑原子谓词$s{\sf -sdp}_k(x_1,y_1,\ldots,x_k,y_k)$，要求不相交路径之间的间距大于某个固定值$s$。采用相同技术，我们证明在有界欧拉亏格图类上，FOL+SDP的模型检验可在二次时间内完成。