Disjoint-paths logic, denoted $\mathsf{FO}$+$\mathsf{dp}$, extends first-order logic ($\mathsf{FO}$) with atomic predicates $\mathsf{dp}_r[(x_1,y_1),\ldots,(x_r,y_r)]$, expressing the existence of vertex-disjoint paths between $x_i$ and $y_i$, for $1\leq i\leq r$. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for $\mathsf{FO}$+$\mathsf{dp}$ is fixed-parameter tractable. This essentially settles the question of tractable model checking for this logic on subgraph-closed classes, since the problem is hard on subgraph-closed classes not excluding a topological minor (assuming a further mild condition of efficiency of encoding).

翻译：不相交路径逻辑，记作 $\mathsf{FO}$+$\mathsf{dp}$，通过引入原子谓词 $\mathsf{dp}_r[(x_1,y_1),\ldots,(x_r,y_r)]$ 扩展了一阶逻辑（$\mathsf{FO}$），该谓词表示对于 $1\leq i\leq r$，在 $x_i$ 和 $y_i$ 之间存在顶点不相交的路径。我们证明，对于每一个排除某个固定图作为拓扑子图的图类，$\mathsf{FO}$+$\mathsf{dp}$ 的模型检验问题是固定参数可解的。这实质上解决了该逻辑在子图封闭类上的可处理模型检验问题，因为该问题在那些不排除拓扑子图的子图封闭类上是困难的（假设存在一个关于编码效率的进一步温和条件）。