
arXiv: 2107.05928
First-order logic (FO) can express many algorithmic problems on graphs, such as the independent set and dominating set problem parameterized by solution size. However, FO cannot express the very simple algorithmic question whether two vertices are connected. We enrich FO with connectivity predicates that are tailored to express algorithmic graph problems that are commonly studied in parameterized algorithmics. By adding the atomic predicates connk(x,y,z_1,..., zk) that hold true in a graph if there exists a path between (the valuations of)xandyafter (the valuations of)z1,..., zkhave been deleted, we obtainseparator logicFO + 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. Denote by FO + connkthe fragment of separator logic that is restricted to connectivity predicates with at mostk + 2variables (that is, at mostkdeletions), we show that FO + connk + 1is strictly more expressive than FO + connkfor allk ≥ 0. 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 strongerdisjoint-paths logicFO + DP by adding the atomic predicates disjoint-pathsk[(x1, y1),..., (xk, yk) that evaluate to true if there are internally vertex-disjoint paths between (the valuations of)xiandyifor all 1 ≤ i ≤ k. Disjoint-paths logic can express the disjoint paths problem, the problem of (topological) minor containment, the problem of hitting (topological) minors, and many more. Again, we show that the fragments FO + DPkthat use predicates for at mostkdisjoint paths form a strict hierarchy of expressiveness. Finally, we compare the expressive power of the new logics with that of transitive-closure logics and monadic second-order logic.
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, graph theory, Model theory of finite structures, 004, Logic in Computer Science (cs.LO), connectivity, Structural characterization of families of graphs, First-order logic, first-order logic, ddc: ddc:004
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, graph theory, Model theory of finite structures, 004, Logic in Computer Science (cs.LO), connectivity, Structural characterization of families of graphs, First-order logic, first-order logic, ddc: ddc:004
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 3 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
