O grupo de pesquisa em "Teoria e Inteligência Computacional" da UFRN, em colaboração com o grupo de pesquisa em "Lógica, Conhecimento e Ética" dá sua contribuição semestral aos Seminários de Lógica e Filosofia Formal da UFRN, com a seguinte programação:
Tema: Especificação e verificação de programas
Palestrante: Isaac de Lima Oliveira Filho
Data de realização: 23 de junho de 2008, 2a-feira, 17h30
Local: sala 3D5
Tema: Lógicas modais e agentes
Palestrante: Anderson Paiva Cruz
Data de realização: 24 de junho de 2008, 3a-feira, 10h30
Local: sala 3D5
Tema: Diagramas de decisão binária
Palestrante: Naiara Silva dos Santos
Data de realização: 25 de junho de 2008, 4a-feira, 17h30
Local: sala 3D5
Tema: Dedução natural, cálculo lambda, e a noção de fórmulas como tipos
Palestrante: Daniel Durante Pereira Alves
Data de realização: 26 de junho de 2008, 5a-feira, 10h30
Local: sala 3D5
ESPECIFICAÇÃO E VERIFICAÇÃO DE PROGRAMAS
-> Isaac de Lima Oliveira Filho
Aplicadas no processo de desenvolvimento de software para a solução de um problema real, as ferramentas fornecidas pelos ditos Métodos Formais podem auxiliar em todas as etapas, desde a abstração, modelagem e *especificação formal* de um programa, que pode ser descrito de forma não ambígua e ter suas propriedades checadas matematicamente, até a *verificação formal* de que tal programa atende à sua especificação, passando ainda pela própria construção de um programa correto diretamente a partir de refinamentos de sua descrição formal original.
O presente seminário se concentrará especificamente sobre a tarefa da verificação formal de programas. Ilustraremos, no caso de programas procedimentais simples, como a abordagem da *lógica de Floyd-Hoare* pode contribuir com uma semântica para programas baseada em pré-condições e pós-condições expressas em lógica de primeira ordem. Explicaremos os conceitos de correção parcial e de correção total de programas, e apresentaremos sistemas dedutivos adequados para o tratamento destes conceitos.
LÓGICAS MODAIS E AGENTES
-> Anderson Paiva Cruz
Uma modalidade é uma expressão de cunho adverbial (tal como 'necessariamente', 'possivelmente', 'obrigatoriamente', 'sabidamente' ou 'eventualmente') que é usada para qualificar a verdade de uma asserção. A Lógica Modal estende a abordagem clássica à lógica pelo estudo do comportamento dedutivo de expressões de caráter modal.
O presente seminário apresentará a sintaxe básica e a semântica padrão de alguns dos principais sistemas de Lógica Modal. Ilustraremos a utilização da Lógica Modal em sistemas multiagentes, em especial no que diz respeito ao raciocínio sobre o conhecimento que tais agentes extraem de seus ambientes e até mesmo sobre o conhecimento que certos agentes possuem sobre outros agentes.
A Lógica Modal se encontra no cerne da pesquisa atual em diversas áreas da ciência da computação, e encontra interessantes aplicações em inteligência artificial, representação do conhecimento, dedução automática, especificação formal de sistemas, engenharia de software, e linguística computacional.
DIAGRAMAS DE DECISÃO BINÁRIA
-> Naiara Silva dos Santos
Diagramas de Decisão Binária (do inglês 'Binary Decision Diagrams' - BDD) são estruturas de dados utilizadas para representar de forma eficiente funções booleanas, formalismos descritivos empregados em muitos sistemas de hardware e software, tais como circuitos síncronos e assíncronos, sistemas reativos e máquinas de estados finitos.
O presente seminário introduzirá o conceito genérico de BDD, bem como sua variante ordenada, e exibirá uma variedade de algoritmos que podem ser usados para a manipulação de BDDs. Ilustraremos ainda parte da ampla quantidade de aplicações atuais que as BDDs encontram na checagem simbólica de modelos para diversos tipos de lógicas, bem como algumas formas de utilização inteligente destas estruturas para evitar certos tipos de problemas potencialmente intratáveis envolvendo “explosões combinatoriais”.
DEDUÇÃO NATURAL, CÁLCULO LAMBDA E A NOÇÃO DE FÓRMULAS COMO TIPOS
-> Daniel Durante Pereira Alves
Dedução Natural é um estilo de formalização lógica bastante estudado, desenvolvido e que propicia diversos tipos de análises dos sistemas de lógica, desde análises mais teórico-filosóficas, em termos dos princípios racionais admitidos nestes sistemas, até análises equivalentes às modelo-teóricas, como correção, completude, consistência entre outras.
Cálculo Lambda é um sistema de notação formal bastante flexível e poderoso, utilizado, entre outras coisas, como fundamento das linguagens de programação funcional, no desenvolvimento de interfaces homem-máquina via linguagem natural, na formalização de teorias matemáticas em sistemas de dedução automática, entre outras aplicações.
A noção de fórmulas-como-tipos, também conhecida como *isomorfismo de Curry-Howard*, vincula de forma surpreendente e rica estes dois "domínios": fórmulas de sistemas lógicos se ligam a tipos de dados, provas formais vinculam-se a programas computacionais; normalização de provas tornam-se processos de computação.
Pretende-se fazer apenas uma apresentação introdutória ao tema.
Nenhum comentário:
Postar um comentário