Provider: DSpace RIS Export
Database: Massey Research Online (MRO) Production Instance
Content: text/plain; charset="UTF-8"
TY - THES
AB - We investigate the expressive power of different fragments of higher-order logics
over finite relational structures (or equivalently, relational databases) with special
emphasis in higher-order logics of order greater than or equal three. Our main results
concern the study of the effect on the expressive power of higher-order logics, of
simultaneously bounding the arity of the higher-order variables and the alternation
of quantifiers. Let AAi(r,m) be the class of (i + 1)-th order logic formulae where
all quantifiers are grouped together at the beginning of the formulae, forming m
alternating blocks of consecutive existential and universal quantifiers, and such that
the maximal-arity (a generalization of the concept of arity, not just the maximal of
the arities of the quantified variables) of the higher-order variables is bounded by r.
Note that, the order of the quantifiers in the prefix may be mixed. We show that,
for every i [greater than or equal to] 1, the resulting AAi hierarchy of formulae of (i + 1)-th order logic is
proper. This extends a result by Makowsky and Pnueli who proved that the same
hierarchy in second-order logic is proper. In both cases the strategy used to prove
the results consists in considering the set AUTOSAT(F) of formulae in a given logic
F which, represented as finite structures, satisfy themselves. We then use a similar
strategy to prove that the classes of [Sigma superscript i subscript m union Pi superscript i subscript m] formulae in which the higher-order
variables of all orders up to i+1 have maximal-arity at most r, also induce a proper
hierarchy in each higher-order logic of order i [greater than or equal to] 3. It is not known whether the
correspondent hierarchy in second-order logic is proper. Using the concept of finite
model truth definitions introduced by M. Mostowski, we give a sufficient condition
for that to be the case. We also study the complexity of the set AUTOSAT(F)
and show that when F is one of the prenex fragments [Sigma superscript 1 subscript m] of second-order logic,
it follows that AUTOSAT(F) becomes a complete problem for the corresponding
prenex fragment [Sigma superscript 2 subscript m] of third-order logic. Finally, aiming to provide the background
for a future line of research in higher-order logics, we take a closer look to the
restricted second-order logic SO[superscript w] introduced by Dawar. We further investigate its
connection with the concept of relational complexity studied by Abiteboul, Vardi
and Vianu. Dawar showed that the existential fragment of SO[superscript w] is equivalent to the
nondeterministic inflationary fixed-point logic NFP. Since NFP captures relational
NP, it follows that the existential fragment of SO[superscript w] captures relational NP. We give
a direct proof, in the style of the proof of Fagin’s theorem, of this fact. We then
define formally the concept of relational machine with relational oracle and prove
the exact correspondence between the prenex fragments of SO[superscript w] and the levels of the
relational polynomial-time hierarchy. This allows us to stablish a direct connection
between the relational polynomial hierarchy and SO without using the Abiteboul
and Vianu normal form for relational machines.
N2 - We investigate the expressive power of different fragments of higher-order logics
over finite relational structures (or equivalently, relational databases) with special
emphasis in higher-order logics of order greater than or equal three. Our main results
concern the study of the effect on the expressive power of higher-order logics, of
simultaneously bounding the arity of the higher-order variables and the alternation
of quantifiers. Let AAi(r,m) be the class of (i + 1)-th order logic formulae where
all quantifiers are grouped together at the beginning of the formulae, forming m
alternating blocks of consecutive existential and universal quantifiers, and such that
the maximal-arity (a generalization of the concept of arity, not just the maximal of
the arities of the quantified variables) of the higher-order variables is bounded by r.
Note that, the order of the quantifiers in the prefix may be mixed. We show that,
for every i [greater than or equal to] 1, the resulting AAi hierarchy of formulae of (i + 1)-th order logic is
proper. This extends a result by Makowsky and Pnueli who proved that the same
hierarchy in second-order logic is proper. In both cases the strategy used to prove
the results consists in considering the set AUTOSAT(F) of formulae in a given logic
F which, represented as finite structures, satisfy themselves. We then use a similar
strategy to prove that the classes of [Sigma superscript i subscript m union Pi superscript i subscript m] formulae in which the higher-order
variables of all orders up to i+1 have maximal-arity at most r, also induce a proper
hierarchy in each higher-order logic of order i [greater than or equal to] 3. It is not known whether the
correspondent hierarchy in second-order logic is proper. Using the concept of finite
model truth definitions introduced by M. Mostowski, we give a sufficient condition
for that to be the case. We also study the complexity of the set AUTOSAT(F)
and show that when F is one of the prenex fragments [Sigma superscript 1 subscript m] of second-order logic,
it follows that AUTOSAT(F) becomes a complete problem for the corresponding
prenex fragment [Sigma superscript 2 subscript m] of third-order logic. Finally, aiming to provide the background
for a future line of research in higher-order logics, we take a closer look to the
restricted second-order logic SO[superscript w] introduced by Dawar. We further investigate its
connection with the concept of relational complexity studied by Abiteboul, Vardi
and Vianu. Dawar showed that the existential fragment of SO[superscript w] is equivalent to the
nondeterministic inflationary fixed-point logic NFP. Since NFP captures relational
NP, it follows that the existential fragment of SO[superscript w] captures relational NP. We give
a direct proof, in the style of the proof of Fagin’s theorem, of this fact. We then
define formally the concept of relational machine with relational oracle and prove
the exact correspondence between the prenex fragments of SO[superscript w] and the levels of the
relational polynomial-time hierarchy. This allows us to stablish a direct connection
between the relational polynomial hierarchy and SO without using the Abiteboul
and Vianu normal form for relational machines.
M3 - Doctoral
M3 - Doctoral
PY - 2008
KW - Relational databases
KW - Computer logic
PB - Massey University
AU - Ferrarotti, Flavio Antonio
TI - Expressibility of higher-order logics on relational databases : proper hierarchies : a dissertation presented in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Information Systems at Massey University, Wellington, New Zealand
LA - en
VL - Doctor of Philosophy (Ph.D.)
DA - 2008
UR - http://hdl.handle.net/10179/799
ER -