Search Results

Documents authored by Pakusa, Wied

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.112
Approximations of Isomorphism and Logics with Linear-Algebraic Operators (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Anuj Dawar, Erich Grädel, and Wied Pakusa

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
Invertible map equivalences are approximations of graph isomorphism that refine the well-known Weisfeiler-Leman method. They are parameterized by a number k and a set Q of primes. The intuition is that two equivalent graphs G equiv^IM_{k, Q} H cannot be distinguished by means of partitioning the set of k-tuples in both graphs with respect to any linear-algebraic operator acting on vector spaces over fields of characteristic p, for any p in Q. These equivalences have first appeared in the study of rank logic, but in fact they can be used to delimit the expressive power of any extension of fixed-point logic with linear-algebraic operators. We define {LA^{k}}(Q), an infinitary logic with k variables and all linear-algebraic operators over finite vector spaces of characteristic p in Q and show that equiv^IM_{k, Q} is the natural notion of elementary equivalence for this logic. The logic LA^{omega}(Q) = Cup_{k in omega} LA^{k}(Q) is then a natural upper bound on the expressive power of any extension of fixed-point logics by means of Q-linear-algebraic operators. By means of a new and much deeper algebraic analysis of a generalized variant, for any prime p, of the CFI-structures due to Cai, Fürer, and Immerman, we prove that, as long as Q is not the set of all primes, there is no k such that equiv^IM_{k, Q} is the same as isomorphism. It follows that there are polynomial-time properties of graphs which are not definable in LA^{omega}(Q), which implies that no extension of fixed-point logic with linear-algebraic operators can capture PTIME, unless it includes such operators for all prime characteristics. Our analysis requires substantial algebraic machinery, including a homogeneity property of CFI-structures and Maschke’s Theorem, an important result from the representation theory of finite groups.
Cite as

Anuj Dawar, Erich Grädel, and Wied Pakusa. Approximations of Isomorphism and Logics with Linear-Algebraic Operators (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 112:1-112:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.ICALP.2019.112,
  author =	{Dawar, Anuj and Gr\"{a}del, Erich and Pakusa, Wied},
  title =	{{Approximations of Isomorphism and Logics with Linear-Algebraic Operators}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{112:1--112:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.112},
  URN =		{urn:nbn:de:0030-drops-106887},
  doi =		{10.4230/LIPIcs.ICALP.2019.112},
  annote =	{Keywords: Finite Model Theory, Graph Isomorphism, Descriptive Complexity, Algebra}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.27
The Model-Theoretic Expressiveness of Propositional Proof Systems

Authors: Erich Grädel, Benedikt Pago, and Wied Pakusa

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory. Specifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded width resolution, and the polynomial calculus of bounded degree, can be characterised in a precise sense by variants of fixed-point logics that are of fundamental importance in descriptive complexity theory. Our main results are that Horn resolution has the same expressive power as least fixed-point logic, that bounded width resolution captures existential least fixed-point logic, and that the (monomial restriction of the) polynomial calculus of bounded degree solves precisely the problems definable in fixed-point logic with counting.
Cite as

Erich Grädel, Benedikt Pago, and Wied Pakusa. The Model-Theoretic Expressiveness of Propositional Proof Systems. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2017.27,
  author =	{Gr\"{a}del, Erich and Pago, Benedikt and Pakusa, Wied},
  title =	{{The Model-Theoretic Expressiveness of Propositional Proof Systems}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{27:1--27:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.27},
  URN =		{urn:nbn:de:0030-drops-76897},
  doi =		{10.4230/LIPIcs.CSL.2017.27},
  annote =	{Keywords: Propositional proof systems, fixed-point logics, resolution, polynomial calculus, generalized quantifiers}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.19
Definability of Cai-Fürer-Immerman Problems in Choiceless Polynomial Time

Authors: Wied Pakusa, Svenja Schalthöfer, and Erkal Selman

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
Choiceless Polynomial Time (CPT) is one of the most promising candidates in the search for a logic capturing Ptime. The question whether there is a logic that expresses exactly the polynomial-time computable properties of finite structures, which has been open for more than 30 years, is one of the most important and challenging problems in finite model theory. The strength of Choiceless Polynomial Time is its ability to perform isomorphism-invariant computations over structures, using hereditarily finite sets as data structures. But, as it preserves symmetries, it is choiceless in the sense that it cannot select an arbitrary element of a set - an operation which is crucial for many classical algorithms. CPT can define many interesting Ptime queries, including (the original version of) the Cai-Fürer-Immerman (CFI) query. The CFI query is particularly interesting because it separates fixed-point logic with counting from Ptime, and has since remained the main benchmark for the expressibility of logics within Ptime. The CFI construction associates with each connected graph a set of CFI-graphs that can be partitioned into exactly two isomorphism classes called odd and even CFI-graphs. The problem is to decide, given a CFI-graph, whether it is odd or even. In the original version, the underlying graphs are linearly ordered, and for this case, Dawar, Richerby and Rossman proved that the CFI query is CPT-definable. However, the CFI query over general graphs remains one of the few known examples for which CPT-definability is open. Our first contribution generalises the result by Dawar, Richerby and Rossman to the variant of the CFI query where the underlying graphs have colour classes of logarithmic size, instead of colour class size one. Secondly, we consider the CFI query over graph classes where the maximal degree is linear in the size of the graphs. For these classes, we establish CPT-definability using only sets of small, constant rank, which is known to be impossible for the general case. In our CFI-recognising procedures we strongly make use of the ability of CPT to create sets, rather than tuples only, and we further prove that, if CPT worked over tuples instead, no such procedure would be definable. We introduce a notion of "sequence-like objects" based on the structure of the graphs' symmetry groups, and we show that no CPT-program which only uses sequence-like objects can decide the CFI query over complete graphs, which have linear maximal degree. From a broader perspective, this generalises a result by Blass, Gurevich, and van den Bussche about the power of isomorphism-invariant machine models (for polynomial time) to a setting with counting.
Cite as

Wied Pakusa, Svenja Schalthöfer, and Erkal Selman. Definability of Cai-Fürer-Immerman Problems in Choiceless Polynomial Time. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{pakusa_et_al:LIPIcs.CSL.2016.19,
  author =	{Pakusa, Wied and Schalth\"{o}fer, Svenja and Selman, Erkal},
  title =	{{Definability of Cai-F\"{u}rer-Immerman Problems in Choiceless Polynomial Time}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{19:1--19:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.19},
  URN =		{urn:nbn:de:0030-drops-65595},
  doi =		{10.4230/LIPIcs.CSL.2016.19},
  annote =	{Keywords: finite model theory, descriptive complexity, logic for textsc\{Ptime\}, Choiceless Polynomial Time, Cai-F\"{u}rer-Immerman}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.390
Rank Logic is Dead, Long Live Rank Logic!

Authors: Erich Grädel and Wied Pakusa

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
Motivated by the search for a logic for polynomial time, we study rank logic (FPR) which extends fixed-point logic with counting (FPC) by operators that determine the rank of matrices over finite fields. While FPR can express most of the known queries that separate FPC from PTIME, nearly nothing was known about the limitations of its expressive power. In our first main result we show that the extensions of FPC by rank operators over different prime fields are incomparable. This solves an open question posed by Dawar and Holm and also implies that rank logic, in its original definition with a distinct rank operator for every field, fails to capture polynomial time. In particular we show that the variant of rank logic FPR* with an operator that uniformly expresses the matrix rank over finite fields is more expressive than FPR. One important step in our proof is to consider solvability logic FPS which is the analogous extension of FPC by quantifiers which express the solvability problem for linear equation systems over finite fields. Solvability logic can easily be embedded into rank logic, but it is open whether it is a strict fragment. In our second main result we give a partial answer to this question: in the absence of counting, rank operators are strictly more expressive than solvability quantifiers.
Cite as

Erich Grädel and Wied Pakusa. Rank Logic is Dead, Long Live Rank Logic!. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 390-404, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2015.390,
  author =	{Gr\"{a}del, Erich and Pakusa, Wied},
  title =	{{Rank Logic is Dead, Long Live Rank Logic!}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{390--404},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.390},
  URN =		{urn:nbn:de:0030-drops-54279},
  doi =		{10.4230/LIPIcs.CSL.2015.390},
  annote =	{Keywords: logic, descriptive complexity, polynomial time, rank logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.213
Definability of linear equation systems over groups and rings

Authors: Anuj Dawar, Erich Grädel, Bjarki Holm, Eryk Kopczynski, and Wied Pakusa

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
Motivated by the quest for a logic for PTIME and recent insights that the descriptive complexity of problems from linear algebra is a crucial aspect of this problem, we study the solvability of linear equation systems over finite groups and rings from the viewpoint of logical (inter-)definability. All problems that we consider are decidable in polynomial time, but not expressible in fixed-point logic with counting. They also provide natural candidates for a separation of polynomial time from rank logics, which extend fixed-point logics by operators for determining the rank of definable matrices and which are sufficient for solvability problems over fields. Based on the structure theory of finite rings, we establish logical reductions among various solvability problems. Our results indicate that all solvability problems for linear equation systems that separate fixed-point logic with counting from PTIME can be reduced to solvability over commutative rings. Further, we prove closure properties for classes of queries that reduce to solvability over rings. As an application, these closure properties provide normal forms for logics extended with solvability operators.
Cite as

Anuj Dawar, Erich Grädel, Bjarki Holm, Eryk Kopczynski, and Wied Pakusa. Definability of linear equation systems over groups and rings. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 213-227, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.CSL.2012.213,
  author =	{Dawar, Anuj and Gr\"{a}del, Erich and Holm, Bjarki and Kopczynski, Eryk and Pakusa, Wied},
  title =	{{Definability of linear equation systems over groups and rings}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{213--227},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.213},
  URN =		{urn:nbn:de:0030-drops-36749},
  doi =		{10.4230/LIPIcs.CSL.2012.213},
  annote =	{Keywords: inite model theory, logics with algebraic operators}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact