Complexidade descritiva da lógica de ponto fixo relacional inflacionário

Abstract

Descriptive Complexity is a field of Finite Model Theory, which is interested in characterizing computational complexity classes in terms of the logical resources that are required to express all the problems belonging to the class. The seminal result in the area is the celebrated Fagin's Theorem, which proves that the class NP is captured by the existential fragment of second order logic. On the other side of the spectrum, we have the well known fact that first-order logic is not sufficiently expressive to define even such simple problems as graph connectivity. The introduction of fixed-point operators is a standard technique to increase the expressive power of a logic in a controlled way. Indeed, Immerman and Vardi prove that first-order logic with the least fixed-point operator, denoted LFP, is able to capture the class P over the set of ordered structures. We generalize the classical fixed-point logics using relations instead of operators. The basic idea is that we use loops in a relation instead of fixed-points of a function, that is, X is a fixed-point of the relation R in case the pair (X,X) belongs to R. We introduce the notion of initial fixed-point of an inflationary relation R and the associated operator rifp. We denote by RIFP the first-order logic with the inflationary relational fixed-point operator rifp and show that it captures the polynomial hierarchy using a translation to second-order logic. We also consider the fragment RIFP1 with the restriction that the rifp operator can be applied at most once. We show that RIFP1 captures the class NP and compare our logic with the nondeterministic fixed-point logic proposed by Abiteboul, Vianu and Vardi, that introduces the notion of non-deterministic fixed-points and proves that the first-order logic with such operators captures the class NP. The results of this work will be published in 11th Workshop on Logical and Semantic Frameworks, with Applications - LSFA.