CoordenaÃÃo de AperfeiÃoamento de Pessoal de NÃvel Superior / NÃs investigamos a teoria dos modelos de LÃgicas Preferenciais, LÃgica HÃbrida
e fragmentos da LÃgica de Segunda-Ordem com relaÃÃo a modelos finitos. A
semÃnticas dessas lÃgicas diferem da abordagem clÃssica pelo uso de relaÃÃes
entre modelos ou por restringir a cardinalidade dos modelos a cardinais finitos.
Este trabalho tem trÃs partes. Na primeira parte deste trabalho nÃs estudamos
a teoria dos modelos de lÃgicas preferenciais. LÃgicas preferenciais
surgem no contexto do raciocÃnio nÃo-monotÃnico em InteligÃncia Artificial. A
principal caracterÃstica dessas lÃgicas à a existÃncia de uma relaÃÃo entre modelos.
Isso permite a definiÃÃo de uma relaÃÃo de consequÃncia nÃo monotÃnica
considerando-se os modelos minimais de um conjunto de sentenÃas. Usando a
abordagem da Teoria dos Modelos Abstrata, nÃs generalizamos alguns resultados
de expressividade para classes de lÃgicas preferenciais. NÃs mostramos que
sempre que uma classe de modelos minimais de um conjunto finito de sentenÃas
à axiomatizÃvel, entÃo tal classe à finitamente axiomatizÃvel. NÃs mostramos
que se tal classe define implicitamente um sÃmbolo do vocabulÃrio, existe uma
axiomatizaÃÃo finita de uma forma particular, a saber, o conjunto finito de
sentenÃas inicial mais uma definiÃÃo explÃcita para o sÃmbolo definido.
Na segunda parte desse trabalho, nÃs investigamos a teoria dos modelos finitos
da LÃgica HÃbrida. LÃgicas HÃbridas sÃo extensÃes da lÃgica modal atravÃs de
termos hÃbridos que se referem a estados individuais em um modelo de Kripke.
NÃs estudamos a complexidade computacional dos problemas de model- e frame-
checking para a LÃgica HÃbrida. NÃs mostramos que para cada problema de
grafos na Hierarquia Polinomial e cada nÃmero n, existe uma fÃrmula que exprime
esse problema para grafos de cardinalidade n. NÃs mostramos que o
tamanho das fÃrmulas à limitado por um polinÃmio em n. NÃs mostramos que
podemos abrir mÃo das modalidades globais se nos limitarmos a grafos conexos
com loops. NÃs definimos fragmentos da LÃgica HÃbrida que correspondem a
cada nÃvel da Hierarquia Polinomial. Isso nos leva a uma prova alternativa da
NP-dificuldade do problema de model-checking para um fragmento especÃfico de
da LÃgica HÃbrida.
Na Ãltima parte desse trabalho, nÃs exploramos a complexidade descritiva
da lÃgica obtida ao restringirmos a quantificaÃÃo de segunda-ordem a relaÃÃes
de grau limitado. Baseados em trabalhos anteriores de Schwentick et al. e
de Grandjean e Olive, nÃs introduzimos a LÃgica de Segunda-Ordem de Grau
Limitado e mostramos que ela captura a classe ALIN de classes de estruturas
unÃrias aceitas por uma mÃquina de acesso randÃmico em tempo linear e um
nÃmero fixo de alternÃncias dependente apenas do problema. NÃs estendemos
essa lÃgica com o operador de fecho transitivo sobre relaÃÃes de ordem superior
sobre relaÃÃes de grau limitado. NÃs mostramos que a LÃgica de Segunda-
Ordem de Grau Limitado com Fecho Transitivo captura quantidade linear de
registradores em uma mÃquina de acesso randÃmico nÃo-determinÃstica onde os
valores armazenados em cada registrador durante a computaÃÃo sÃo limitados
por uma funÃÃo linear na cardinalidade da estrutura de entrada. / We investigate the model theory of Preferential Logics, Hybrid Logic and fragments
of Second-Order Logic with respect to finite models. The semantics of
these logics differ from the semantics of classical logics either by using relations
between models or by restricting the cardinality of the models considered.
This work has three main parts. In the first part of this work we study
the model theory of preferential logics. Preferential logics arise in the context
of nonmonotonic reasoning in Artificial Intelligence. The main characteristic
of those logics is the existence of a relation between models. It allows the
definition of a nonmonotonic consequence relation by considering the minimal
models of a set of sentences. Using the approach of Abstract Model Theory
we generalize some expressiveness results to classes of preferential logics. We
show that whenever a class of minimal models of a finite set of sentences is
axiomatizable, without considering the preference relation, then it is finitely
axiomatizable. We also show that when such class of minimal models implicitly
defines a symbol, then the finite axiomatization can be put in a very specic
form, namely, the initial set of sentences plus a explicit definition for the symbol.
In the second part of this work, we investigate the finite model theory of
Hybrid Logic. Hybrid Logics are extensions of modal logics with hybrid terms
which refer to single states in a Kripke model. We study the complexity of
the model- and frame-checking problems for Hybrid Logic. We show that for
each graph problem in the Polynomial Hierarchy and each natural number n
there is a formula which expresses this problem for graphs of cardinality n. We
also show that the size of such formulas is bounded by a polynomial in n. We
show that one can disregard the global modalities if one consider only connected
graphs with loops. We define fragments which correspond to each degree of the
Polynomial Hierarchy. This leads to an alternative proof of the NP-hardness of
the model-checking problem for an specic fragment of Full Hybrid Logic.
In the last part of this work, we explore the descriptive complexity of the
logic obtained by restricting second-order quantication to relations of bounded
degree. Based on previous work from Schwentick et al. and Grandjean and
Olive, we introduce the Bounded-Degree Second-Order Logic and show that it
captures the class ALIN of classes of unary structures accepted by a alternating
random access machine in linear time and bounded number of alternations. We
also extend this logic with the transitive closure operator on high-order relations
on bounded-degree relations. We show that the Bounded-Degree Second-Order
Logic with Transitive Closure Operator captures linear number of registers in
a nondeterministic random access machine provided that registers store values
bounded by a linear function in the cardinality of the input structure.
| Identifer | oai:union.ndltd.org:IBICT/oai:www.teses.ufc.br:6280 |
| Date | 07 December 2012 |
| Creators | Francicleber Martins Ferreira |
| Contributors | Ana Teresa de Castro Martins, Marcelino Cavalcante Pequeno, Carlos Eduardo Fisch de Brito, Mario Roberto Folhadela Benevides, Edward Hermann Hauesler, Erich Gradel |
| Publisher | Universidade Federal do CearÃ, Programa de PÃs-GraduaÃÃo em CiÃncia da ComputaÃÃo, UFC, BR |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Format | application/pdf |
| Source | reponame:Biblioteca Digital de Teses e Dissertações da UFC, instname:Universidade Federal do Ceará, instacron:UFC |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0031 seconds