Decidable Expansions of Labelled Linear Orderings

Word Automaticity of Tree Automatic Scattered Linear Orderings Is Decidable

A tree automatic structure is a structure whose domain can be encoded by a regular tree language such that each relation is recognisable by a finite automaton processing tuples of trees synchronously. Words can be regarded as specific simple trees and a structure is word automatic if it is encodable using only these trees. The question naturally arises whether a given tree automatic structure is already word automatic. We prove that this problem is decidable for tree automatic scattered linear orderings. Moreover, we show that in case of a positive answer a word automatic presentation is compu…

Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering

We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the $Σ_1$ theory is undecidable (already over two letters). We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations. We prove that when at most two variables are not alternation bounded, the $Σ_1$ fragment is decidable, and that it becomes undecidable when three variab…

Monadic second-order definable graph orderings

We study the question of whether, for a given class of finite graphs, one can define, for each graph of the class, a linear ordering in monadic second-order logic, possibly with the help of monadic parameters. We consider two variants of monadic second-order logic: one where we can only quantify over sets of vertices and one where we can also quantify over sets of edges. For several special cases, we present combinatorial characterisations of when such a linear ordering is definable. In some cases, for instance for graph classes that omit a fixed graph as a minor, the presented conditions are …

有界线性团宽度的标记良拟序类

Labelled Well Quasi Ordered Classes of Bounded Linear Clique-Width

本文提出算法判定顶点带有限标记的有限图类在诱导子图关系下是否良拟序，并在有界线性团宽度假设下证明了Pouzet猜想，同时给出Daliagault等人早期结果的新证明。

具有可判定一元二阶理论的无限词与双无限词

Infinite and Bi-infinite Words with Decidable Monadic Theories

研究无限词与双无限词的可判定一元二阶理论，给出递归ω-词集合的Σ3-完全性，转移特征刻画，证明驯服谓词存在于各图灵度，并确定不可区分谓词数量，揭示两类词的逻辑性质异同。

HORPO with Computability Closure : A Reconstruction

This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability clo- sure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types.