License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2020.23
URN: urn:nbn:de:0030-drops-116661
Go to the corresponding LIPIcs Volume Portal

Grange, Julien ; Segoufin, Luc

Order-Invariant First-Order Logic over Hollow Trees

LIPIcs-CSL-2020-23.pdf (0.5 MB)


We show that the expressive power of order-invariant first-order logic collapses to first-order logic over hollow trees. A hollow tree is an unranked ordered tree where every non leaf node has at most four adjacent nodes: two siblings (left and right) and its first and last children. In particular there is no predicate for the linear order among siblings nor for the descendant relation. Moreover only the first and last nodes of a siblinghood are linked to their parent node, and the parent-child relation cannot be completely reconstructed in first-order.

BibTeX - Entry

  author =	{Julien Grange and Luc Segoufin},
  title =	{{Order-Invariant First-Order Logic over Hollow Trees}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Maribel Fern{\'a}ndez and Anca Muscholl},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-116661},
  doi =		{10.4230/LIPIcs.CSL.2020.23},
  annote =	{Keywords: order-invariance, first-order logic}

Keywords: order-invariance, first-order logic
Collection: 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Issue Date: 2020
Date of publication: 06.01.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI