| Summary: | FARIAS, Márcia Roberta Falcão de. Complexidade descritiva da lógica de ponto fixo relacional inflacionário. 2016. 114 f. Tese (Doutorado em Ciência da Computação)-Universidade Federal do Ceará, Fortaleza, 2016. === Submitted by Anderson Silva Pereira (anderson.pereiraaa@gmail.com) on 2017-01-10T20:51:08Z
No. of bitstreams: 1
2016_tese_mrffarias.pdf: 875367 bytes, checksum: b080a902e479415aafe748ca7f2224e9 (MD5) === Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2017-01-11T15:46:49Z (GMT) No. of bitstreams: 1
2016_tese_mrffarias.pdf: 875367 bytes, checksum: b080a902e479415aafe748ca7f2224e9 (MD5) === Made available in DSpace on 2017-01-11T15:46:49Z (GMT). No. of bitstreams: 1
2016_tese_mrffarias.pdf: 875367 bytes, checksum: b080a902e479415aafe748ca7f2224e9 (MD5)
Previous issue date: 2016 === 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. === Complexidade Descritiva é um ramo da Teoria dos Modelos Finitos que está interessada em caracterizar classes de complexidade computacionais em termos dos recursos lógicos necessários para expressar todos os problemas que estão contidos na classe. O resultado mais celebrado da área é o Teorema de Fagin que prova que a classe NP é capturada pelo fragmento existencial de segunda ordem. Por outro lado, a lógica de primeira ordem (FO) não é expressiva o suficiente para definir problemas simples como o problema da conectividade de grafos. A introdução de operadores de ponto fixo é uma técnica padrão para acrescentar poder expressivo à lógica de maneira controlada. De fato, Immerman e Vardi provam que FO com o operador de menor ponto fixo, denotada por LFP, é capaz de capturar a classe P sobre estruturas finitas e ordenadas. Neste trabalho, seguiremos uma abordagem diferente e definiremos a noção de ponto fixo sobre uma relação arbitrária. Nós generalizamos as lógicas clássicas de ponto fixo usando relações no lugar de operadores. A ideia básica é que usamos laços em uma relação no lugar de pontos fixos de uma função, isto é, X é ponto fixo de uma relação R no caso do par (X,X) pertencer à relação R. Nós introduzimos a noção de ponto fixo inicial de uma relação inflacionária R e o operador rifp associado. Chamamos de RIFP a lógica FO com o operador de ponto fixo relacional inflacionário e mostramos que essa lógica captura a hierarquia polinomial usando uma tradução para a lógica de segunda ordem. Também consideramos o fragmento RIFP1 com a restrição do operador rifp poder ser aplicado no máximo uma vez. Mostramos que RIFP1 captura a classe NP e comparamos nossa lógica com a lógica de ponto fixo não-determinístico proposta por Abiteboul, Vianu e Vardi, que introduz a noção do ponto fixo não-determinístico e prova que a lógica FO com o operador de ponto fixo não-determinístico captura a classe NP sobre estruturas ordenadas. Os resultados deste trabalho foram aceitos para publicação em 11th Workshop on Logical and Semantic Frameworks, with Applications - LSFA.
|
|---|
