2006 | OriginalPaper | Buchkapitel
First-Order and Counting Theories of ω-Automatic Structures
verfasst von : Dietrich Kuske, Markus Lohrey
Erschienen in: Foundations of Software Science and Computation Structures
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The logic
${\mathcal L}({\mathcal Q}_u)$
extends first-order logic by a generalized form of counting quantifiers (“the number of elements satisfying ... belongs to the set
C
”). This logic is investigated for structures with an injective
ω
-automatic presentation. If first-order logic is extended by an infinity-quantifier, the resulting theory of any such structure is known to be decidable [4]. It is shown that, as in the case of automatic structures [13], also modulo-counting quantifiers as well as infinite cardinality quantifiers (“there are
$\varkappa$
many elements satisfying ...”) lead to decidable theories. For a structure of bounded degree with injective
ω
-automatic presentation, the fragment of
${\mathcal L}({\mathcal Q}_u)$
that contains only effective quantifiers is shown to be decidable and an elementary algorithm for this decision is presented. Both assumptions (
ω
-automaticity and bounded degree) are necessary for this result to hold.