Schirrmacher, Nicole ;
Siebertz, Sebastian ;
Vigny, Alexandre
FirstOrder Logic with Connectivity Operators
Abstract
Firstorder 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 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 conn_k(x,y,z_1,…,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,…,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 firstorder definable classes. Denote by FO+conn_k the fragment of separator logic that is restricted to connectivity predicates with at most k+2 variables (that is, at most k deletions). We show that FO+conn_{k+1} is strictly more expressive than FO+conn_k for all k ≥ 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 stronger disjointpaths logic FO+DP by adding the atomic predicates disjointpaths_k[(x_1,y_1),…,(x_k,y_k)] that evaluate to true if there are internally vertexdisjoint paths between (the valuations of) x_i and y_i for all 1 ≤ i ≤ k. Disjointpaths 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+DP_k that use predicates for at most k disjoint paths form a strict hierarchy of expressiveness. Finally, we compare the expressive power of the new logics with that of transitiveclosure logics and monadic secondorder logic.
BibTeX  Entry
@InProceedings{schirrmacher_et_al:LIPIcs.CSL.2022.34,
author = {Schirrmacher, Nicole and Siebertz, Sebastian and Vigny, Alexandre},
title = {{FirstOrder Logic with Connectivity Operators}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {34:134:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772181},
ISSN = {18688969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/15754},
URN = {urn:nbn:de:0030drops157548},
doi = {10.4230/LIPIcs.CSL.2022.34},
annote = {Keywords: Firstorder logic, graph theory, connectivity}
}
27.01.2022
Keywords: 

Firstorder logic, graph theory, connectivity 
Seminar: 

30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Issue date: 

2022 
Date of publication: 

27.01.2022 