O Departamento de Filosofia da UFRN, através da Base de Pesquisa "Lógica, Conhecimento e Ética", dá continuidade a sua programação anual dos Seminários de Lógica e Filosofia Formal, com a palestra:
O conceito de verdade nas línguas naturais
Prof. André Leclerc
Departamento de Filosofia - UFPB
Data: 29/08/2008 às 16 h.
Local: UFRN, Setor II, sala D1
quinta-feira, 21 de agosto de 2008
terça-feira, 17 de junho de 2008
Os novos mundos do cosmo
O Departamento de Filosofia da UFRN, através da Base de Pesquisa "Lógica, Conhecimento e Ética", dá continuidade a sua programação anual dos Seminários de Lógica e Filosofia Formal, com a palestra:
Os novos mundos do cosmo
Prof. José Renan de Medeiros
Departamento de Física - UFRN
Data: 27/06/2008 às 16h
Local: UFRN, Setor II, sala C1
Os novos mundos do cosmo
Prof. José Renan de Medeiros
Departamento de Física - UFRN
Data: 27/06/2008 às 16h
Local: UFRN, Setor II, sala C1
segunda-feira, 16 de junho de 2008
SEMANA DA LÓGICA, na UFRN (2008.1)
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.
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.
quarta-feira, 28 de maio de 2008
Lógica e arte
O Departamento de Filosofia da UFRN, através da Base de Pesquisa "Lógica, Conhecimento e Ética", dá continuidade a sua programação anual dos Seminários de Lógica e Filosofia Formal, com a palestra:
Lógica e arte
Prof. Daniel Durante P. Alves
Departamento de Filosofia - UFRN
Data: 06/06/2008 às 16h
Local: UFRN, Setor II, sala C1
Lógica e arte
Prof. Daniel Durante P. Alves
Departamento de Filosofia - UFRN
Data: 06/06/2008 às 16h
Local: UFRN, Setor II, sala C1
sexta-feira, 18 de abril de 2008
Da retórica à sócio-retórica
O Departamento de Filosofia da UFRN, através da Base de Pesquisa "Lógica, Conhecimento e Ética", dá inicio a sua programação anual dos Seminários de Lógica e Filosofia Formal, com a palestra:
Da retórica à sócio-retórica
Prof. Alzir Oliveira - Departamento de Letras - UFRN
Data: 25/04/2008 às 16h
Local: UFRN, Setor II, sala C1
Da retórica à sócio-retórica
Prof. Alzir Oliveira - Departamento de Letras - UFRN
Data: 25/04/2008 às 16h
Local: UFRN, Setor II, sala C1
terça-feira, 18 de março de 2008
Argumentação e Lógica Informal
O Departamento de Filosofia da UFRN, através da Base de Pesquisa "Lógica, Conhecimento e Ética", dá inicio a sua programação anual dos Seminários de Lógica e Filosofia Formal, com a palestra:
Argumentação e Lógica Informal
Prof. Desidério Murcho - Instituto de Filosofia, Artes e Cultura - UFOP
Data: 28/03/2008 às 16h
Local: UFRN, Auditório B do CCET
Argumentação e Lógica Informal
Prof. Desidério Murcho - Instituto de Filosofia, Artes e Cultura - UFOP
Data: 28/03/2008 às 16h
Local: UFRN, Auditório B do CCET
segunda-feira, 3 de dezembro de 2007
SEMANA DA LÓGICA, na UFRN (2007.2)
Mais uma realização do grupo de pesquisa da UFRN em
"Lógica e Filosofia Formal".
Estão todos convidados!
Tema: Fundamentos da demonstração automática de teoremas
Palestrante: João Marcos
Data de realização: 10/12/07, 2a-feira, 18h30
Local: anfiteatro B do CCET
Resumo:
Esta palestra fará uma breve introdução histórica e conceitual à área de demonstração assistida ou automática de teoremas. Os fundamentos teóricos relacionados à programação funcional e à lógica de ordem superior servirão de base para uma apresentação ao ambiente computacional de demonstração *Isabelle*.
Tema: Matemática Discreta Aplicada
Palestrante: Lucas Cavalcante
Data de realização: 11/12/07, 3a-feira, 18h30
Local: anfiteatro B do CCET
Resumo:
Nesta palestra veremos como lidar com objetos fundamentais da Matemática Discreta no ambiente de demonstração assistida de teoremas *Isabelle*. O objetivo é expor uma similaridade entre demonstrações implementadas com o auxílio da ferramenta *Isabelle* e aquelas realizadas da maneira usual, à mão. Abordaremos conceitos como funções recursivas, conjuntos parcialmente ordenados, princípio da indução e estruturas de dados em forma de listas.
Tema: Dedução Natural em *Isabelle*
Palestrante: Dalmo Mendonça
Data de realização: 12/12/07, 4a-feira, 18h30
Local: anfiteatro B do CCET
Resumo:
Demonstrações de teoremas por dedução natural no sistema *Isabelle* podem ser feitas da maneira usual: aplicando regras de inferência. A garantia da correção é um ponto forte do sistema. Será apresentada a teoria correspondente à Lógica Clássica Proposicional e será mostrado como criar regras de inferências derivadas e regras de abreviatura. A maior vantagem do *Isabelle* aparece no uso de técnicas avançadas, os taticais, que são comandos que permitem automatizar parcialmente ou totalmente as demonstrações.
Tema: Uma introdução ao Cálculo Lambda
Palestrante: Talis Lincoln
Data de realização: 13/12/07, 5a-feira, 16h30
Local: anfiteatro B do CCET
Resumo:
Nesta palestra será apresentado o Cálculo Lambda, um sistema formal desenvolvido para estudar definições e aplicações de funções. Mostraremos conceitos, regras, definições e notações do Cálculo Lambda. Serão discutidos ainda as grandes semelhanças com linguagens de programação funcional, em particular SML, e a estreita relação existente entre programas de computador e demonstrações matemáticas, fenômeno conhecido como isomorfismo de Curry-Howard.
"Lógica e Filosofia Formal".
Estão todos convidados!
Tema: Fundamentos da demonstração automática de teoremas
Palestrante: João Marcos
Data de realização: 10/12/07, 2a-feira, 18h30
Local: anfiteatro B do CCET
Resumo:
Esta palestra fará uma breve introdução histórica e conceitual à área de demonstração assistida ou automática de teoremas. Os fundamentos teóricos relacionados à programação funcional e à lógica de ordem superior servirão de base para uma apresentação ao ambiente computacional de demonstração *Isabelle*.
Tema: Matemática Discreta Aplicada
Palestrante: Lucas Cavalcante
Data de realização: 11/12/07, 3a-feira, 18h30
Local: anfiteatro B do CCET
Resumo:
Nesta palestra veremos como lidar com objetos fundamentais da Matemática Discreta no ambiente de demonstração assistida de teoremas *Isabelle*. O objetivo é expor uma similaridade entre demonstrações implementadas com o auxílio da ferramenta *Isabelle* e aquelas realizadas da maneira usual, à mão. Abordaremos conceitos como funções recursivas, conjuntos parcialmente ordenados, princípio da indução e estruturas de dados em forma de listas.
Tema: Dedução Natural em *Isabelle*
Palestrante: Dalmo Mendonça
Data de realização: 12/12/07, 4a-feira, 18h30
Local: anfiteatro B do CCET
Resumo:
Demonstrações de teoremas por dedução natural no sistema *Isabelle* podem ser feitas da maneira usual: aplicando regras de inferência. A garantia da correção é um ponto forte do sistema. Será apresentada a teoria correspondente à Lógica Clássica Proposicional e será mostrado como criar regras de inferências derivadas e regras de abreviatura. A maior vantagem do *Isabelle* aparece no uso de técnicas avançadas, os taticais, que são comandos que permitem automatizar parcialmente ou totalmente as demonstrações.
Tema: Uma introdução ao Cálculo Lambda
Palestrante: Talis Lincoln
Data de realização: 13/12/07, 5a-feira, 16h30
Local: anfiteatro B do CCET
Resumo:
Nesta palestra será apresentado o Cálculo Lambda, um sistema formal desenvolvido para estudar definições e aplicações de funções. Mostraremos conceitos, regras, definições e notações do Cálculo Lambda. Serão discutidos ainda as grandes semelhanças com linguagens de programação funcional, em particular SML, e a estreita relação existente entre programas de computador e demonstrações matemáticas, fenômeno conhecido como isomorfismo de Curry-Howard.
Assinar:
Postagens (Atom)