Abstract:We survey the definitions and main properties of first-order (FO) definable unary operations on relational structures, called FO-transductions, and of FO-definable binary operations based on disjoint union and Cartesian product. We focus our study on Backwards Translation Theorems and Splitting Theorems that permit to express FO properties of output structures in terms of finitely many FO properties of the corresponding input ones.
In the particular cases where the operations are defined by quantifier-free (QF) formulas, the quantifier-heights of the obtained sentences are no larger than those of the input ones. It follows that the class of finite models of a FO sentence is recognizable with respect to the considered QF operations. Recognizability has interesting algorithmic properties based on finite automata on terms, for structures having bounded tree-width or clique-width.
We extend our results to FO sentences constructed with modulo counting existential quantifiers.
From: Bruno Courcelle [view email]
[v1]
Fri, 29 May 2026 12:55:03 UTC (156 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。