2022/11/03 by Petr A. Golovach, Golovach, Petr A., Giannos Stamoulis +3 · 1 citation
Chemistry · Computer Science · #03C13 #05C83 #05C85 #68Q19 #68Q25 #68Q27 #68R10 #68W01 #Combinatorics (math.CO) #Data Structures and Algorithms (cs.DS) #F.2.2 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #G.2.2 #Logic in Computer Science (cs.LO) #Organometallic Complex Synthesis and Catalysis #Synthetic Organic Chemistry Methods
paper · pdf · doi:10.48550/arxiv.2211.01723
openalex publication_date 2022/11/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The disjoint paths logic, FOL+DP, is an extension of First-Order Logic (FOL) with the extra atomic predicate dpk(x1,y1,…,xk,yk), expressing the existence of internally vertex-disjoint paths between xi and yi, for i∈\1,…, 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 -sdpk(x1,y1,…,xk,yk), 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.