The AGM paradigm [1] is a theory about how idealized rational agents should change their beliefs when receiving new information. This paradigm has been successfully applied to families of logics satisfying certain common assumptions, such as compactness. For non-compact logics, there are still no general results that can be used. We investigate the application of the AGM paradigm to temporal logics, more specifically, to Linear-time Temporal Logic (LTL) [3]. As many temporal logics, LTL is not compact, and hence, one cannot use the general results described in [2]. We show that the simple definition of an AGM partial meet contraction for sets of LTL formulas is an undecidable problem. We discuss possible ways to address this problem and show that under certain restrictions, it is possible to correctly define an operator of partial meet contraction. Although we focus on LTL for the sake of clarity, the undecidability result also holds for others temporal and dynamic logics, such as CTL and PDL .

As abordagens de Teoria da Argumentação, subárea de Representação do Conhecimento, visam compreender e modelar raciocínio como um processo de construção de argumentos seguida de avaliação das relações de conflito ou co-consistência entre os mesmos. Entre as abordagens mais fundamentais da área, encontramos Argumentação Abstrata (Abstract Argumentation) e Argumentação Baseada em Suposições (Assumption-Based Argumentation), ambas originais da década de 90 e fundamentadas nas tradicionais semânticas de Programação em Lógica (Logic Programming). Apresentaremos nesta oportunidade nosso trabalho contínuo de comparação entre os três formalismos e os avanços que obtivemos em função de compreender suas diferenças.

Nessa apresentação, vamos analisar a complexidade parametrizada de fragmentos decidíveis da lógica de primeira-ordem. A complexidade computacional da satisfatibilidade para diversos desses fragmentos é alta em geral. Estudar o problema da perspectiva da Complexidade Parametrizada permite verificar que, para situações particulares, a complexidade do problema pode ser considerada tratável.

O objetivo deste trabalho é investigar o seguinte problema para uma classe de estruturas finitas fixada C: dado dois conjuntos finitos P e N de estruturas em C e um inteiro positivo r, encontrar uma fórmula de primeira-ordem com quantifier rank no máximo r que seja satisfeita por todas as estruturas em P e por nenhuma estrutura em N. Nós consideramos as seguintes classes de estruturas: estruturas de conjunto, estruturas de relações unárias, estruturas de equivalência, ordens lineares, uniões disjuntas de ordens lineares e strings. Utilizamos resultados do jogo Ehrenfeucht–Fraïssé nessas classes de estruturas para garantir que a fórmula pode ser obtida em tempo polinomial no tamanho da entrada P, N e r.

Planejamento Automatizado é a área da Inteligência Artificial que se preocupa com o processo de elaboração de um plano de ações para o alcance de metas. Em aplicações práticas, as ações possuam efeitos incertos, isto é, não determinı́sticos. Soluções para problemas de planejamento não-determinı́stico são baseadas na abordagem de verificação simbólica de modelos. Abordagens tradicionais de verificação simbólica de modelos são baseadas na lógica CTL (Computation Tree Logic). Entretanto, esta lógica não considera as ações que causam as transições entre estados e, por este motivo, não é adequada para representar problemas de planejamento. Assim, nesta apresentação, mostraremos uma lógica mais adequada para representar problemas de planejamento, a lógica α-CTL. Além disso, apresentaremos os algoritmos de verificação de modelos simbólica que estãos sendo desenvolvidos para solucionar problemas de planejamento sob incerteza.

Planejamento Automatizado é uma subárea da Inteligência Artificial que se preocupa com a escolha de ações de um agente inteligente para alcançar uma meta. Uma solução para um problema de planejamento é uma sequência de ações (plano), que leva o agente de um estado inicial a um estado que satisfaz a meta (estado meta). No entanto, nem sempre é possível obter um plano para o problema de planejamento. Neste caso, dizemos que o problema de planejamento não possui solução. Nesta apresentação, mostraremos como a teoria de Revisão de Crenças pode ser utilizada para fundamentar as mudanças minimais em problemas de planejamento sem solução a fim de torná-los solucionáveis. Mostraremos ainda ideias em estudo de métricas de revisão que levam em consideração informações sobre os problemas, tais como preferências no alcance das metas e relevância de proposições.