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.

FERREIRA, Francicleber Martins. Expressividade e complexidade em lógicas preferenciais, híbridas e de grau limitado. 2012. 130 f. Tese (Doutorado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2012. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-20T11:58:10Z No. of bitstreams: 1 2012_tese_fmferreira.pdf: 772301 bytes, checksum: b1e1a404221e38ffb8e0712513749a4c (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-25T11:47:07Z (GMT) No. of bitstreams: 1 2012_tese_fmferreira.pdf: 772301 bytes, checksum: b1e1a404221e38ffb8e0712513749a4c (MD5) / Made available in DSpace on 2016-07-25T11:47:07Z (GMT). No. of bitstreams: 1 2012_tese_fmferreira.pdf: 772301 bytes, checksum: b1e1a404221e38ffb8e0712513749a4c (MD5) Previous issue date: 2012 / 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. / 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.

La symétrie est par définition un concept multidisciplinaire. Il apparaît dans de nombreux domaines. En général, elle revient à une transformation qui laisse invariant un objet. Le problème de satisfaisabilité (SAT) occupe un rôle central en théorie de la complexité. Il est le problème de décision de référence de la classe NP-complet (Cook, 71). Il consiste à déterminer si une formule CNF admet ou non une valuation qui la rend vraie. Dans la première contribution de ce mémoire, nous avons introduit une nouvelle méthode complète qui élimine toutes les symétries locales pour la résolution du problème SAT en exploitant son groupe des symétries. Les résultats obtenus montrent que l'exploitation des symétries locales est meilleure que l'exploitation des symétries globales sur certaines instances SAT et que les deux types de symétries sont complémentaires, leur combinaison donne une meilleure exploitation.En deuxième contribution, nous proposons une approche d'apprentissage de clauses pour les solveurs SAT modernes en utilisant les symétries. Cette méthode n'élimine pas les modèles symétriques comme font les méthodes statiques d'élimination des symétries. Elle évite d'explorer des sous-espaces correspondant aux no-goods symétriques de l'interprétation partielle courante. Les résultats obtenus montrent que l'utilisation de ces symétries et ce nouveau schéma d'apprentissage est profitable pour les solveurs CDCL.En Intelligence Artificielle, on inclut souvent la non-monotonie et l'incertitude dans le raisonnement sur les connaissances avec exceptions. Pour cela, en troisième et dernière contribution, nous avons étendu la notion de symétrie à des logiques non classiques (non-monotones) telles que les logiques préférentielles, les X-logiques et les logiques des défauts.Nous avons montré comment raisonner par symétrie dans ces logiques et nous avons mis en évidence l'existence de certaines symétries dans ces logiques qui n'existent pas dans les logiques classiques. / Symmetry is by definition a multidisciplinary concept. It appears in many fields. In general, it is a transformation which leaves an object invariant. The problem of satisfiability (SAT) is one of the central problems in the complexity theory. It is the first decision Np-complete problem (Cook, 71). It deals with determining if a CNF formula admits a valuation which makes it true. First we introduce a new method which eliminates all the local symmetries during the resolution of a SAT problem by exploiting its group of symmetries. Our experimental results show that for some SAT instances, exploiting local symmetries is better than exploiting just global symmetries and both types of symmetries are complementary. As a second contribution, we propose a new approach of Conflict-Driven Clause Learning based on symmetry. This method does not eliminate the symmetrical models as the static symmetry elimination methods do. It avoids exploring sub-spaces corresponding to symmetrical No-goods of the current partial interpretation. Our experimental results show that using symmetries in clause learning is advantageous for CDCL solvers.In artificial intelligence, we usually include non-monotony and uncertainty in the reasoning on knowledge with exceptions. Finally, we extended the concept of symmetry to non-classical logics that are preferential logics, X-logics and default logics. We showed how to reason by symmetry in these logics and we prove the existence of some symmetries in these non-classical logics which do not exist in classical logics.