First-order Logic with Connectivity Operators

DOI10.1145/3595922MaRDI QIDQ6082227zbMATH OpenOpenAlexWikidataFDO

Authors Sebastian Siebertz, Alexandre Vigny

Publication date 3 November 2023

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2107.05928

zbMATH Keywords

connectivityfirst-order logicgraph theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Abstract: First-order logic (FO) can express many algorithmic problems on graphs, such as the independent set and dominating set problem, parameterized by solution size. On the other hand, FO cannot express the very simple algorithmic question of whether two vertices are connected. We enrich FO with connectivity predicates that are tailored to express algorithmic graph properties that are commonly studied in parameterized algorithmics. By adding the atomic predicates $con{n}_k(x,y,z_1,ldots,z_k)$ that hold true in a graph if there exists a path between (the valuations of) $x$ and $y$ after (the valuations of) $z_1,ldots,z_k$ have been deleted, we obtain separator logic $FO+conn$. We show that separator logic can express many interesting problems such as the feedback vertex set problem and elimination distance problems to first-order definable classes. We then study the limitations of separator logic and prove that it cannot express planarity, and, in particular, not the disjoint paths problem. We obtain the stronger disjoint-paths logic $FO+DP$ by adding the atomic predicates $disjoint-path{s}_k[(x_1,y_1),ldots,(x_k,y_k)]$ that evaluate to true if there are internally vertex disjoint paths between (the valuations of) $x_i$ and $y_i$ for all $1leilek$. Disjoint-paths logic can express the disjoint paths problem, the problem of (topological) minor containment, the problem of hitting (topological) minors, and many more. Finally, we compare the expressive power of the new logics with that of transitive closure logics and monadic second-order logic.

Recommendations

• First-Order Logic with Connectivity Operators
• scientific article; zbMATH DE number 1163943
• Where first-order and monadic second-order logic coincide
• Where first-order and monadic second-order logic coincide
• On monadic NP vs monadic co-NP

Cites work

• A fixed-parameter tractable algorithm for elimination distance to bounded degree graphs
• Algebra for trees
• An algorithmic meta-theorem for graph modification to planarity and FOL
• Directed Nowhere Dense Classes of Graphs
• Elements of finite model theory.
• Elimination Distance to Bounded Degree on Planar Graphs
• Elimination distances, blocking sets, and kernels for Vertex Cover
• Finding odd cycle transversals.
• Finite model theory and its applications.
• First-order logic with reachability for infinite-state systems
• First-order logic with reachability predicates on infinite systems
• Fixed-parameter tractable distances to sparse graph classes
• Graph isomorphism parameterized by elimination distance to bounded degree
• Graph minors. V. Excluding a planar graph
• Graph minors. XIII: The disjoint paths problem
• Graph minors. XX: Wagner's conjecture
• Hitting topological minors is FPT
• scientific article; zbMATH DE number 3819693 (Why is no real title available?)
• scientific article; zbMATH DE number 3474957 (Why is no real title available?)
• scientific article; zbMATH DE number 1324669 (Why is no real title available?)
• scientific article; zbMATH DE number 1759688 (Why is no real title available?)
• scientific article; zbMATH DE number 2086614 (Why is no real title available?)
• scientific article; zbMATH DE number 863496 (Why is no real title available?)
• Linear time solvable optimization problems on graphs of bounded clique-width
• Logic, graphs, and algorithms
• Lower bounds on the complexity of \(\mathsf{MSO}_1\) model-checking
• Minimum bisection is fixed-parameter tractable
• Parameterized algorithms
• Parameterized complexity of elimination distance to first-order logic properties
• Regular graphs of large girth and arbitrary degree
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• Vertex deletion parameterized by elimination distance and even less
• Weak Second‐Order Arithmetic and Finite Automata

Cited in

(6)

• First-Order Logic with Connectivity Operators
• Elimination distance to bounded degree on planar graphs preprint
• Model checking disjoint-paths logic on topological-minor-free graph classes
• Compound logics for modification problems
• Advances in algorithmic meta theorems (invited paper)
• Elimination distance to dominated clusters

This page was built for publication: First-order Logic with Connectivity Operators

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6082227)