O LoLITA (grupo de "Lógica, Linguagem, Informação, Teoria e Aplicações") do DIMAp/UFRN, em colaboração com o grupo de pesquisa em "Lógica, Conhecimento e Ética" do DeFil/UFRN, dá sua contribuição semestral aos Seminários de Lógica e Filosofia Formal da UFRN, com a seguinte programação:
Tema: Lógica Combinatória e Cálculo Lambda
Palestrante: Plácido Antônio de Souza Neto
Data: 15 de dezembro de 2008, 2a-feira, 18h30
Tema: Cálculo Lambda e Isomorfismo de Curry-Howard
Palestrante: Cléverton Hentz Antunes
Data: 16 de dezembro de 2008, 3a-feira, 18h30
Tema: Lógica Modal
Palestrante: Haniel Moreira Barbosa
Data: 17 de dezembro de 2008, 4a-feira, 18h30
Tema: Lógica Intuicionista
Palestrante: Otto Luis Pontes Soares de Araújo
Data: 18 de dezembro de 2008, 5a-feira, 18h30
Todas as palestras serão realizadas no auditório do CCET/UFRN.
quarta-feira, 10 de dezembro de 2008
quinta-feira, 4 de dezembro de 2008
Reasoning about Dynamic Depth Profiles
------------------------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-------------------------------------------------------------------------------------------
Título: Reasoning about Dynamic Depth Profiles
Palestrante: Paulo E. Santos (FEI)
Data: 08/12/2008, 14h30
Local: Sala 03B, IME-USP
Abstract: Reasoning about perception of depth and about spatial
relations between moving physical objects is a challenging problem.
We investigate the representation of depth and motion
by means of depth profiles whereby each object in the world
is represented as a single peak. We propose a logical theory,
formulated in the situation calculus (SC), that is used for reasoning
about object motion (including motion of the observer).
The theory proposed here is comprehensive enough to accommodate reasoning
about both sensor data and actions in the world. We show that
reasoning about depth profiles is sound and complete with
respect to actual motion in the world.
This shows that in the conceptual neighbourhood diagram (CND) of
all possible depth perceptions, the transitions between perceptions are
logical consequences of the proposed theory of depth and motion.
At the end of the talk I'll present some current work on the integration of
probabilistic reasoning in this framework.
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-------------------------------------------------------------------------------------------
Título: Reasoning about Dynamic Depth Profiles
Palestrante: Paulo E. Santos (FEI)
Data: 08/12/2008, 14h30
Local: Sala 03B, IME-USP
Abstract: Reasoning about perception of depth and about spatial
relations between moving physical objects is a challenging problem.
We investigate the representation of depth and motion
by means of depth profiles whereby each object in the world
is represented as a single peak. We propose a logical theory,
formulated in the situation calculus (SC), that is used for reasoning
about object motion (including motion of the observer).
The theory proposed here is comprehensive enough to accommodate reasoning
about both sensor data and actions in the world. We show that
reasoning about depth profiles is sound and complete with
respect to actual motion in the world.
This shows that in the conceptual neighbourhood diagram (CND) of
all possible depth perceptions, the transitions between perceptions are
logical consequences of the proposed theory of depth and motion.
At the end of the talk I'll present some current work on the integration of
probabilistic reasoning in this framework.
terça-feira, 2 de dezembro de 2008
Verdade em Gottlob Frege
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:
Verdade em Gottlob Frege
Prof. Fernando Raul Neto
Departamento de Filosofia, UFPE
Data: 12/12/2008 às 16h
Local: UFRN, Setor II, sala D1
Verdade em Gottlob Frege
Prof. Fernando Raul Neto
Departamento de Filosofia, UFPE
Data: 12/12/2008 às 16h
Local: UFRN, Setor II, sala D1
sexta-feira, 28 de novembro de 2008
"O Cisne Negro"
---------- Forwarded message ----------
From: Alvaro Augusto Waldrigues de Almeida
Date: 2008/11/27
Subject: [Ct] Convite para palestra: "O Cisne Negro"
Dando continuidade ao programa de palestras da UTFPR/DAELT, venho
convidá-los para a palestra "O Cisne Negro: ciência, filosofia, os
limites do conhecimento e o impacto do altamente improvável".
Data: 01/12/2008
Horário: 19h30min às 21h20min
Palestrante: Alvaro Augusto de Almeida
Local: Mini-auditório do campus Curitiba da Universidade Tecnológica
Federal do Paraná (UTFPR). Av. Sete de Setembro, 3165, Curitiba, PR
O assunto tem a ver com nossa incapacidade de prever acontecimentos
futuros e está relacionado, dentre outras coisas, à recente crise
financeira mundial (um "cisne cinzento") e à intensificação da
globalização (aumento da complexidade). Alguns pontos que serão
abordados são:
1. Eventos do tipo "cisne negro" e a impossibilidade de prever o futuro.
2. O princípio da refutabilidade de Popper e os limites do
conhecimento científico.
3. O inconsciente freudiano e a impossibilidade de "prever" o presente.
4. Caos e complexidade: as ciências exatas não são tão exatas assim.
5. Os teoremas da incompletude de Gödel: nem a matemática pura escapa!
Atenciosamente,
Prof. Alvaro Augusto de Almeida
Universidade Tecnológica Federal do Paraná - UTFPR
Departamento Acadêmico de Eletrotécnica - DAELT
http://alvaroaugusto.blogspot.com
http://maquinas-utfpr.blogspot.com
Date: 2008/11/27
Subject: [Ct] Convite para palestra: "O Cisne Negro"
Dando continuidade ao programa de palestras da UTFPR/DAELT, venho
convidá-los para a palestra "O Cisne Negro: ciência, filosofia, os
limites do conhecimento e o impacto do altamente improvável".
Data: 01/12/2008
Horário: 19h30min às 21h20min
Palestrante: Alvaro Augusto de Almeida
Local: Mini-auditório do campus Curitiba da Universidade Tecnológica
Federal do Paraná (UTFPR). Av. Sete de Setembro, 3165, Curitiba, PR
O assunto tem a ver com nossa incapacidade de prever acontecimentos
futuros e está relacionado, dentre outras coisas, à recente crise
financeira mundial (um "cisne cinzento") e à intensificação da
globalização (aumento da complexidade). Alguns pontos que serão
abordados são:
1. Eventos do tipo "cisne negro" e a impossibilidade de prever o futuro.
2. O princípio da refutabilidade de Popper e os limites do
conhecimento científico.
3. O inconsciente freudiano e a impossibilidade de "prever" o presente.
4. Caos e complexidade: as ciências exatas não são tão exatas assim.
5. Os teoremas da incompletude de Gödel: nem a matemática pura escapa!
Atenciosamente,
Prof. Alvaro Augusto de Almeida
Universidade Tecnológica Federal do Paraná - UTFPR
Departamento Acadêmico de Eletrotécnica - DAELT
http://alvaroaugusto.blogspot.com
http://maquinas-utfpr.blogspot.com
Real-Time Dynamic Programming
------------------------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-------------------------------------------------------------------------------------------
Título: Real-Time Dynamic Programming
Palestrante: Renato Schattan Pereira Coelho
Data: 01/12/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
O problema de tomada automática de decisão em geral envolve a questão de levar o
agente de um estado inicial a estados com alguma característica de nosso
interesse (estados meta) com o menor custo possível. Assim, queremos que o
agente seja capaz de, para cada estado do mundo, escolher uma ação que minimize
o custo esperado de se chegar a um estado meta, ou seja, queremos definir uma
política que mapeie estados às melhores ações que o agente deve executar.
Uma das abordagens que tem conseguido mais sucesso na resolução desses
problemas, tanto teoricamente quanto em competições de planejamento
probabilístico, é a de programação dinâmica com atualizações assíncronas dos
valores dos estados.
Neste seminário vamos apresentar o algoritmo Real-Time Dynamic Programming
(RTDP), e duas de suas extensões (LRTDP, FRTDP e BRTDP), cuja idéia básica é
fazer várias simulações da execução de uma política gulosa (como se o agente
estivesse treinando) e
atualizar os valores dos estado enquanto se faz a simulação. Por fim, vamos
falar brevemente sobre as alterações que devem ser feitas em um desses
algoritmos (LRTDP) para que ele resolva problemas em que as probabilidades de
transição de estados não são totalmente conhecidas.
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-------------------------------------------------------------------------------------------
Título: Real-Time Dynamic Programming
Palestrante: Renato Schattan Pereira Coelho
Data: 01/12/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
O problema de tomada automática de decisão em geral envolve a questão de levar o
agente de um estado inicial a estados com alguma característica de nosso
interesse (estados meta) com o menor custo possível. Assim, queremos que o
agente seja capaz de, para cada estado do mundo, escolher uma ação que minimize
o custo esperado de se chegar a um estado meta, ou seja, queremos definir uma
política que mapeie estados às melhores ações que o agente deve executar.
Uma das abordagens que tem conseguido mais sucesso na resolução desses
problemas, tanto teoricamente quanto em competições de planejamento
probabilístico, é a de programação dinâmica com atualizações assíncronas dos
valores dos estados.
Neste seminário vamos apresentar o algoritmo Real-Time Dynamic Programming
(RTDP), e duas de suas extensões (LRTDP, FRTDP e BRTDP), cuja idéia básica é
fazer várias simulações da execução de uma política gulosa (como se o agente
estivesse treinando) e
atualizar os valores dos estado enquanto se faz a simulação. Por fim, vamos
falar brevemente sobre as alterações que devem ser feitas em um desses
algoritmos (LRTDP) para que ele resolva problemas em que as probabilidades de
transição de estados não são totalmente conhecidas.
domingo, 23 de novembro de 2008
SPUDD: usando Diagramas de Decisão para resolver Processos Markovianos de Decisão fatorados.
------------------------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-------------------------------------------------------------------------------------------
Título:
SPUDD: usando Diagramas de Decisão para resolver Processos Markovianos de
Decisão fatorados.
Palestrante: Karina Valdivia Delgado (estudante de doutorado IME)
Data: 24/11/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
Planejamento probabilístico é uma sub-área de planejamento da Inteligência
Artificial que usa Processos Markovianos de Decisão (MDPs) como modelo
matemático. MDPs fornecem um arcabouço matemático para modelar e resolver
problemas de decisão sequencial com incerteza em ambientes completamente
observáveis.
Um MDP modela a interação entre um agente e seu ambiente. A cada instante o
agente faz uma escolha de ações (com efeitos probabilísticos) e decide executar
uma ação que produzirá um estado futuro e uma recompensa. O objetivo do agente é
maximizar a recompensa ganha ao longo de uma sequência de escolhas de ações.
Uma das dificuldades para resolver um problema MDP é que frequentemente o
tamanho do espaço de estados é muito grande. Resultados recentes têm
demonstrado que é possível resolver uma formulação fatorada de um MDP chamada de
MDP-fatorado numa maneira mais eficiente (com millões de estados) quando
comparados com soluções clássicas baseados em programação dinâmica e com o
espaço de estados enumerativo.
Nesta palestra mostraremos o algoritmo SPUDD em que os estados são agregados
implicitamente usando ADDs (diagramas de decisão algébricos) para representar a
função valor e as políticas, evitando assim trabalhar com o espaço de estados
enumerativos. SPUDD modifica o algoritmo clássico de iteração de valor usando
ADDs permitindo que o cálculo do valor esperado e as maximizações sejam feitas
eficientemente.
--
Marcelo Finger
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-------------------------------------------------------------------------------------------
Título:
SPUDD: usando Diagramas de Decisão para resolver Processos Markovianos de
Decisão fatorados.
Palestrante: Karina Valdivia Delgado (estudante de doutorado IME)
Data: 24/11/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
Planejamento probabilístico é uma sub-área de planejamento da Inteligência
Artificial que usa Processos Markovianos de Decisão (MDPs) como modelo
matemático. MDPs fornecem um arcabouço matemático para modelar e resolver
problemas de decisão sequencial com incerteza em ambientes completamente
observáveis.
Um MDP modela a interação entre um agente e seu ambiente. A cada instante o
agente faz uma escolha de ações (com efeitos probabilísticos) e decide executar
uma ação que produzirá um estado futuro e uma recompensa. O objetivo do agente é
maximizar a recompensa ganha ao longo de uma sequência de escolhas de ações.
Uma das dificuldades para resolver um problema MDP é que frequentemente o
tamanho do espaço de estados é muito grande. Resultados recentes têm
demonstrado que é possível resolver uma formulação fatorada de um MDP chamada de
MDP-fatorado numa maneira mais eficiente (com millões de estados) quando
comparados com soluções clássicas baseados em programação dinâmica e com o
espaço de estados enumerativo.
Nesta palestra mostraremos o algoritmo SPUDD em que os estados são agregados
implicitamente usando ADDs (diagramas de decisão algébricos) para representar a
função valor e as políticas, evitando assim trabalhar com o espaço de estados
enumerativos. SPUDD modifica o algoritmo clássico de iteração de valor usando
ADDs permitindo que o cálculo do valor esperado e as maximizações sejam feitas
eficientemente.
--
Marcelo Finger
quinta-feira, 13 de novembro de 2008
Revising Specifications with CTL Properties using Bounded Model Checking
==========================================
Adolfo Neto
Departamento Acadêmico de Informática
Universidade Tecnológica Federal do Paraná
Fone: (41) 3310-4644 / Fax: (41) 3310-4646
Web: http://www.dainf.ct.utfpr.edu.br/~adolfo
Blog: http://professoradolfo.blogspot.com
==========================================
---------- Forwarded message ----------
From: Marcelo Finger <mfinger@ime.usp.br>
Date: Thu, Nov 13, 2008 at 2:27 PM
Subject: Seminário LIAMF dia 17/11/2008
To: liamf-anuncios@ime.usp.br
Cc: liamf-seminarios@ime.usp.br
Título: Revising Specifications with CTL Properties using Bounded Model Checking
Palestrantes: Marcelo Finger e Renata Wassermann
Data: 17/11/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
During the process of software development, it is very common that
inconsistencies arise between the formal specification and some
desired property. Belief Revision deals with the problem of
accommodating new information that may be inconsistent with an
existing knowledge base.
In this paper, we propose the use of belief revision techniques in
order to deal with inconsistencies in formal specifications. The
main problem to be solved is that the most well known results for
belief revision only hold for logics which are monotonic and
compact, while most discrete-time temporal logics used to
express system properties -- and in particular, CTL --- are not
compact. We suggest the use of bounded model-checking, transforming
the problem from CTL into classical propositional logic and then
transforming back the results to suggest revisions to the user.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
From: Marcelo Finger <mfinger@ime.usp.br>
Date: Thu, Nov 13, 2008 at 2:27 PM
Subject: Seminário LIAMF dia 17/11/2008
To: liamf-anuncios@ime.usp.br
Cc: liamf-seminarios@ime.usp.br
Título: Revising Specifications with CTL Properties using Bounded Model Checking
Palestrantes: Marcelo Finger e Renata Wassermann
Data: 17/11/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
During the process of software development, it is very common that
inconsistencies arise between the formal specification and some
desired property. Belief Revision deals with the problem of
accommodating new information that may be inconsistent with an
existing knowledge base.
In this paper, we propose the use of belief revision techniques in
order to deal with inconsistencies in formal specifications. The
main problem to be solved is that the most well known results for
belief revision only hold for logics which are monotonic and
compact, while most discrete-time temporal logics used to
express system properties -- and in particular, CTL --- are not
compact. We suggest the use of bounded model-checking, transforming
the problem from CTL into classical propositional logic and then
transforming back the results to suggest revisions to the user.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
sábado, 8 de novembro de 2008
"Semantical completeness, categoricity and logical consequence: an unpublished lecture by Tarski (1940)"
==================================
Palestra sobre Filosofia da Lógica
==================================
Palestra sobre Filosofia da Lógica
==================================
Prof. Paolo Mancosu
Department of Philosophy
University of California, Berkeley
"Semantical completeness, categoricity and logical consequence: an
unpublished lecture by Tarski (1940)"
Resumo:
In the Tarski archive at Berkeley there is a lecture entitled "On the
Completeness and Categoricity of Deductive Systems" that Tarski had
intended to publish but never did. The lecture is an important
historical document for the development of abstract notions of
semantics, such as semantical completeness and categoricity. In
addition, the lecture provides welcome information on a topic of central
interest to Tarski and to contemporary philosophy of logic, e.g. the
Tarskian notion of logical consequence. Finally, some of the technical
problems raised in the lecture, concerning semantical completeness and
categoricity in higher order logic, are still open and have very
recently been the object of renewed attention. In my talk I will spell
out the key elements in the lecture and provide extensive commentary
with the aim of clarifying the conceptual background of the lecture and
to point to the relevance of some of the issues discussed by Tarski to
contemporary philosophical and logical discussions.
Data e Local:
CLE (Centro de Lógica, Epistemologia e História da Ciência)
Sala 209
Quinta-feira 13/11, 14hs
Ficam todos convidados!
Marcelo Coniglio
DF/IFCH e CLE
Unicamp
quinta-feira, 6 de novembro de 2008
Alternating-time Temporal Logic, Coalition Logic and STIT theory of agency and their epistemic extensions
-----------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: Alternating-time Temporal Logic, Coalition Logic and STIT theory of
agency and their epistemic extensions
Palestrante: Andreas Herzig (prof. Visitante IME-USP), IRIT-CNRS (Toulouse,
France)
Data: 10/11/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
Alternating-time Temporal Logic (ATL), Coalition Logic and so-called STIT
theories of agency (`seeing-to-it-that') are three different formalisms to
model the capability of agents and groups of agents to ensure some
outcome. While they come from 3 different traditions (theoretical computer
science, game theory and philosophy of action), in all of them the notion
of independence of agents is fundamental. I shall give an overview, and
explain that only STIT theories allow to reason about uniform strategies,
i.e. strategies where it does not suffice that the agent has the
capability to ensure some fact, but he must also know that he has that
ability.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: Alternating-time Temporal Logic, Coalition Logic and STIT theory of
agency and their epistemic extensions
Palestrante: Andreas Herzig (prof. Visitante IME-USP), IRIT-CNRS (Toulouse,
France)
Data: 10/11/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
Alternating-time Temporal Logic (ATL), Coalition Logic and so-called STIT
theories of agency (`seeing-to-it-that') are three different formalisms to
model the capability of agents and groups of agents to ensure some
outcome. While they come from 3 different traditions (theoretical computer
science, game theory and philosophy of action), in all of them the notion
of independence of agents is fundamental. I shall give an overview, and
explain that only STIT theories allow to reason about uniform strategies,
i.e. strategies where it does not suffice that the agent has the
capability to ensure some fact, but he must also know that he has that
ability.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
segunda-feira, 3 de novembro de 2008
"Observaçoes sobre o teorema do ponto fixo de Gödel"
Quarta-feira, dia 05/11/2008, 16h, sala de seminários (209) do CLE-Unicamp.
Seminário de Rodrigo Freire, doutorando no CLE-Unicamp.
sábado, 1 de novembro de 2008
Ontological Engineering and its Applications (emphasis in Educational Contexts)
-----------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: Ontological Engineering and its Applications (emphasis in Educational
Contexts)
Palestrante: Seiji Isotani
Department of Knowledge Systems
ISIR, Osaka University, Japan
http://www.ei.sanken.osaka-u.ac.jp/~isotani
Data: 3/11/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
In recent years, with the increasing use of technology, Artificial
Intelligence has been gradually and successfully introduced into
a variety of systems (including educational ones). However, major
challenges still remain. Among these, we are interested in how to
represent the knowledge of intelligent authoring systems and then how
to use this knowledge efficiently. Usual approaches to such issues
provide their systems with a kind of expertise using a set of
heuristics and domain theories built-in the procedures (programming
languages). This means that the programmers, not the systems, have an
understanding about the knowledge being used. To deal with this
problem, we will show some of the efforts the ontology engineering
community has been done in order to create better intelligent systems.
First of all, we will try to create a basic common understanding about
the difference between heavy- and light-weight ontologies. Then, we
will explain the research being done in Japan to define heavy-weight
ontologies that support the development of intelligent systems.
Finally, we will present the development of an ontology for Education
used to support collaborative learning and its results to (a) produce
semantically-enabled intelligent systems; and (b) help instructors to
design effective collaboration in real scenarios.
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: Ontological Engineering and its Applications (emphasis in Educational
Contexts)
Palestrante: Seiji Isotani
Department of Knowledge Systems
ISIR, Osaka University, Japan
http://www.ei.sanken.osaka-u.ac.jp/~isotani
Data: 3/11/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
In recent years, with the increasing use of technology, Artificial
Intelligence has been gradually and successfully introduced into
a variety of systems (including educational ones). However, major
challenges still remain. Among these, we are interested in how to
represent the knowledge of intelligent authoring systems and then how
to use this knowledge efficiently. Usual approaches to such issues
provide their systems with a kind of expertise using a set of
heuristics and domain theories built-in the procedures (programming
languages). This means that the programmers, not the systems, have an
understanding about the knowledge being used. To deal with this
problem, we will show some of the efforts the ontology engineering
community has been done in order to create better intelligent systems.
First of all, we will try to create a basic common understanding about
the difference between heavy- and light-weight ontologies. Then, we
will explain the research being done in Japan to define heavy-weight
ontologies that support the development of intelligent systems.
Finally, we will present the development of an ontology for Education
used to support collaborative learning and its results to (a) produce
semantically-enabled intelligent systems; and (b) help instructors to
design effective collaboration in real scenarios.
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
sexta-feira, 24 de outubro de 2008
Alternating-time Temporal Logic, Coalition Logic and STIT theory of agency and their epistemic extensions
-----------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: Alternating-time Temporal Logic, Coalition Logic and STIT theory of
agency and their epistemic extensions
Palestrante: Andreas Herzig (prof. Visitante IME-USP), IRIT-CNRS (Toulouse,
France)
Data: 27/10/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
Alternating-time Temporal Logic (ATL), Coalition Logic and so-called STIT
theories of agency (`seeing-to-it-that') are three different formalisms to
model the capability of agents and groups of agents to ensure some
outcome. While they come from 3 different traditions (theoretical computer
science, game theory and philosophy of action), in all of them the notion
of independence of agents is fundamental. I shall give an overview, and
explain that only STIT theories allow to reason about uniform strategies,
i.e. strategies where it does not suffice that the agent has the
capability to ensure some fact, but he must also know that he has that
ability.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: Alternating-time Temporal Logic, Coalition Logic and STIT theory of
agency and their epistemic extensions
Palestrante: Andreas Herzig (prof. Visitante IME-USP), IRIT-CNRS (Toulouse,
France)
Data: 27/10/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
Alternating-time Temporal Logic (ATL), Coalition Logic and so-called STIT
theories of agency (`seeing-to-it-that') are three different formalisms to
model the capability of agents and groups of agents to ensure some
outcome. While they come from 3 different traditions (theoretical computer
science, game theory and philosophy of action), in all of them the notion
of independence of agents is fundamental. I shall give an overview, and
explain that only STIT theories allow to reason about uniform strategies,
i.e. strategies where it does not suffice that the agent has the
capability to ensure some fact, but he must also know that he has that
ability.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
sábado, 18 de outubro de 2008
Depuração de programas baseada em modelos: uma abordagem hierárquica
-----------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: Depuração de programas baseada em modelos: uma abordagem hierárquica
Palestrante: Wellington Pinheiro
Data: 20/10/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
Diagnóstico baseado em modelos (Model based diagnosis - MBD) é uma técnica
de Inteligência Artificial usada para encontrar componentes falhos em
dispositivos físicos (sistemas). MBD também tem sido utilizado para auxiliar
programadores experientes a encontrarem falhas em seus programas, sendo essa
técnica chamada de depuração de programas baseada em modelos (Model
based software debugging - MBSD). Embora o MBSD possa auxiliar programadores
experientes a entenderem e corrigirem seus erros, essa abordagem precisa ser
aprimorada para aprendizes de programação.
Nesse seminário, mostraremos uma proposta de uso da técnica de diagnóstico
hierárquico para dar suporte a aprendizes de programação explorando a idéia de
componentes abstratos, tais como: padrões elementares, funções e
procedimentos. Com a utilização de uma abordagem de diagnóstico hierárquico,
será possível encontrar falhas no programa do aluno em diversos níveis de
abstração. Com isso, espera-se que o aluno seja capaz de compreender a origem
de seus erros e aprender durante esse processo.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: Depuração de programas baseada em modelos: uma abordagem hierárquica
Palestrante: Wellington Pinheiro
Data: 20/10/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
Diagnóstico baseado em modelos (Model based diagnosis - MBD) é uma técnica
de Inteligência Artificial usada para encontrar componentes falhos em
dispositivos físicos (sistemas). MBD também tem sido utilizado para auxiliar
programadores experientes a encontrarem falhas em seus programas, sendo essa
técnica chamada de depuração de programas baseada em modelos (Model
based software debugging - MBSD). Embora o MBSD possa auxiliar programadores
experientes a entenderem e corrigirem seus erros, essa abordagem precisa ser
aprimorada para aprendizes de programação.
Nesse seminário, mostraremos uma proposta de uso da técnica de diagnóstico
hierárquico para dar suporte a aprendizes de programação explorando a idéia de
componentes abstratos, tais como: padrões elementares, funções e
procedimentos. Com a utilização de uma abordagem de diagnóstico hierárquico,
será possível encontrar falhas no programa do aluno em diversos níveis de
abstração. Com isso, espera-se que o aluno seja capaz de compreender a origem
de seus erros e aprender durante esse processo.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
quarta-feira, 15 de outubro de 2008
Existência e Verdade
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 mesa redonda:
Existência e Verdade
Prof. João Branquinho - Universidade de Lisboa
Prof. Cláudio Ferreira Costa - UFRN
Prof. Daniel Durante Alves - UFRN (moderador)
Data: 22/10/2008 às 19h
Local: UFRN, CHLA, Auditório da Filosofia
Existência e Verdade
Prof. João Branquinho - Universidade de Lisboa
Prof. Cláudio Ferreira Costa - UFRN
Prof. Daniel Durante Alves - UFRN (moderador)
Data: 22/10/2008 às 19h
Local: UFRN, CHLA, Auditório da Filosofia
quarta-feira, 8 de outubro de 2008
An optimal method for reasoning about actions
-----------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: An optimal method for reasoning about actions
Palestrante: Andreas Herzig (prof. Visitante IME-USP), IRIT-CNRS (Toulouse,
France)
Data: 13/10/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
(paper with Hans van Ditmarsch and Tiago de Lima "Optimal regression for
reasoning about knowledge and actions" at AAAI'07; later version available
at http://drops.dagstuhl.de/portals/index.php?semnr=07351)
The frame problem is one of the major obstacles on the road towards
logical reasoning about actions in AI. Two versions can be distinguished.
The representational version is the problem of designing a logical
language and a semantics such that domains can be described without
stating all the non-effects of each action. The inferential version is to
design an efficient reasoning method for a given solution to the
representational problem. Several solutions to the representational
problem where proposed in the past. The solution of Reiter (1991), further
extended by Scherl and Levesque (1993), relies on the hypothesis of
inertia: each action only changes the truth value of a small number of
facts, leaving all the others unchanged. Reiter's associated regression
inference method eliminates action symbols from formulas by rewriting them
to formulas of propositional logic (or formulas of epistemic logic in
Scherl and Levesque's case). In the general case, however, the regressed
formula may be exponentially larger than the original formula, and hence
non-optimal. We here present the first optimal reasoning method for
Reiter's and Scherl and Levesque's solution. We first show that their
solution to the representational frame problem can be encoded into dynamic
epistemic logic of van Ditmarsch, van der Hoek and Kooi (2005). We then
give a polynomial reduction to epistemic logic. We also establish some
complexity results for our reasoning method: NP-completeness for a single
agent, PSPACE-completeness for multiple agents, and EXPTIME-completeness
when common knowledge is involved.
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: An optimal method for reasoning about actions
Palestrante: Andreas Herzig (prof. Visitante IME-USP), IRIT-CNRS (Toulouse,
France)
Data: 13/10/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
(paper with Hans van Ditmarsch and Tiago de Lima "Optimal regression for
reasoning about knowledge and actions" at AAAI'07; later version available
at http://drops.dagstuhl.de/portals/index.php?semnr=07351)
The frame problem is one of the major obstacles on the road towards
logical reasoning about actions in AI. Two versions can be distinguished.
The representational version is the problem of designing a logical
language and a semantics such that domains can be described without
stating all the non-effects of each action. The inferential version is to
design an efficient reasoning method for a given solution to the
representational problem. Several solutions to the representational
problem where proposed in the past. The solution of Reiter (1991), further
extended by Scherl and Levesque (1993), relies on the hypothesis of
inertia: each action only changes the truth value of a small number of
facts, leaving all the others unchanged. Reiter's associated regression
inference method eliminates action symbols from formulas by rewriting them
to formulas of propositional logic (or formulas of epistemic logic in
Scherl and Levesque's case). In the general case, however, the regressed
formula may be exponentially larger than the original formula, and hence
non-optimal. We here present the first optimal reasoning method for
Reiter's and Scherl and Levesque's solution. We first show that their
solution to the representational frame problem can be encoded into dynamic
epistemic logic of van Ditmarsch, van der Hoek and Kooi (2005). We then
give a polynomial reduction to epistemic logic. We also establish some
complexity results for our reasoning method: NP-completeness for a single
agent, PSPACE-completeness for multiple agents, and EXPTIME-completeness
when common knowledge is involved.
domingo, 5 de outubro de 2008
Construção de mapas semânticos com robôs móveis
-----------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: Construção de mapas semânticos com robôs móveis
Palestrante: Fabiano Rogério Corrêa
Data: 06/10/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
A robótica móvel teve um avanço considerável na última década devido ao
emprego de modelos probabilísticos e técnicas de aprendizado computacional.
Hoje em dia é possível mapear de maneira eficiente e robusta um ambiente e
simultaneamente localizar o robô móvel, apenas com as informações espaciais
obtidas de seus sensores. No entanto, novos desafios estão sendo abordados
na área, e a incorporação de informação semântica (classificação das
informações espaciais) vem sendo adotada por alguns pesquisadores como a
direção a ser seguida na solução dos problemas.
Nessa palestra será exposto um panorama dos trabalhos mais recentes na área
de construção de mapas semânticos, seguida de uma indicação de que modelos
probabilísticos de primeira ordem possibilitam um melhor tratamento da
natureza relacional dos dados obtidos pelos robôs móveis para classificação
semântica.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
sexta-feira, 26 de setembro de 2008
Densidade e bolas fechadas em análise de agrupamentos
-----------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: Densidade e bolas fechadas em análise de agrupamentos
Palestrante: Carlos Gonzalez
Data: 29/09/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
-------
Uma das conceitualizações possíveis em análise de agrupamentos
consiste em selecionar as áreas do espaço de características (feature
space) que apresentam maior densidade. O conceito básico de densidade
surge de considerar a quantidade
de pontos que tem uma determinada região do espaço. Seguindo com esta linha de
raciocínio, precisamos determinar, de alguma maneira, a região que vai ser
considerada para calcular a densidade.
Neste sentido, noções topológicas bem conhecidas, como a de bola
fechada, podem nos auxiliar. Mas para isto precisamos analisar o
seguinte problema: dado um conjunto de elementos do espaço de
características: como determinar uma bola
fechada mínima ou minimal que inclua este conjunto? Uma vez solucionado este
problema, podemos pensar várias maneiras de aplicar este contexto metodológico
em análise de agrupamentos. Se trabalharmos em análise de agrupamentos
hierárquico acumulativo, podemos determinar que dois agrupamentos
A_{1} e A_{2} serão selecionados para formar um novo agrupamento se a
densidade da menor bola fechada que inclui A_{1} e A_{2} tem a maior
densidade ou uma densidade maximal. Denominamos a este algoritmo
``grande bola''. Também podemos usar alguma noção de distância para
determinar, para cada par de agrupamentos A_{1} e A_{2} o conjunto E
dos elementos de A_{1} e A_{2} que estão mais próximos, considerando
para a seleção de agrupamentos a densidade da menor menor bola fechada
que inclua E. Este algoritmo é denominado ``bola no meio''.
A principal vantagem (o que na realidade foi a motivação inicial)
consiste em que a generalidade de aplicação destes conceitos permite
comparar tipos de espaços e noções de noções de distância muito
diferentes. Neste trabalho, usamos este enfoque conceitual e os
algoritmos mencionados para comparar o conhecido espaço métrico que
usa a noção de distância de Jaccard com os espaços booleanos,
nos quais as distâncias são elementos da mesma álgebra de Boole usada como
espaço de características.
São mostrados alguns resultados experimentais para uma comparação inicial deste
enfoque.
Todos são benvindos
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
quinta-feira, 25 de setembro de 2008
Towards the self-regulation of personality-based social exchange processes in multiagent systems
O grupo de pesquisa em "Teoria e Inteligência Computacional" da UFRN tem o prazer de anunciar a palestra:
Towards the self-regulation of personality-based social exchange processes in multiagent systems
Prof. Graçaliz Dimuro
Universidade Católica de Pelotas
Data: 26/09/2008 às 14h
Local: UFRN, DIMAp, sala de reuniões
Abstract:
The regulation of agent interactions based on Piaget's theory of social exchanges was first proposed by Dimuro and Costa in 2005. According to that theory, social interactions are seen as service exchanges between pairs of agents and the qualitative evaluation of those exchanges by the agents by means of social exchange values: the investment value for performing a service or the satisfaction value for receiving it. The exchanges also generate values of debts and credits that help to guarantee the continuity of future interactions. A multiagent system (MAS) is said to be in social equilibrium if the balances of investment and satisfaction values are equilibrated for the successive exchanges occurring along the time. A (centralized) mechanism for the regulation of social exchanges in MAS, based on the concept of equilibrium supervisor with an associated Qualitative Interval Markov Decision Process (QI-MDP) was introduced in 2005. This approach was extended to consider personality-based agents in 2006.
We are now going towards the (distributed) self-regulation of personality-based social exchanges, by decentralizing the equilibrium supervisor through the internalization of its decision process in the interacting agents. For simplicity, we consider that the exchanges between each pair of agents have no influence from the exchanges occurring between other pair of agents, which allowed for a simple way of distributing the decision process. However, since the agents do not necessarily have access to the internal states (balances of exchange values) of each other, the decision processes have to operate in a partially observable mode, by means of Partially Observable Markov Models POMDP).
The decision about the best exchanges that an agent should propose to its partner in order to achieve social equilibrium, or to promote new interactions, is modeled as a global POMDP for each personality trait that its partner may assume. Considering a set of six personality traits (egoism, strong egoism, altruism, strong altruism, tolerance, equilibrium fanaticism), each global POMDP is decomposed into three sub-POMDPs, according to the current internal state (favorable, equilibrated or unfavorable balance of material exchange values) of the agent that is supervising the interaction.
For convenience, we have chosen the BDI architecture for the agents in the social exchange simulator used in this work. We developed an algorithm to extract BDI plans from the policy graphs of each sub-POMDP, building a set of rules that form the BDI plans for interacting with agents of each personality model. Those plans are to be selected in each interaction according to the current balance of material values of the agents in each exchange stage. Such plans are said to ``obey'' optimal POMDP policies.
Towards the self-regulation of personality-based social exchange processes in multiagent systems
Prof. Graçaliz Dimuro
Universidade Católica de Pelotas
Data: 26/09/2008 às 14h
Local: UFRN, DIMAp, sala de reuniões
Abstract:
The regulation of agent interactions based on Piaget's theory of social exchanges was first proposed by Dimuro and Costa in 2005. According to that theory, social interactions are seen as service exchanges between pairs of agents and the qualitative evaluation of those exchanges by the agents by means of social exchange values: the investment value for performing a service or the satisfaction value for receiving it. The exchanges also generate values of debts and credits that help to guarantee the continuity of future interactions. A multiagent system (MAS) is said to be in social equilibrium if the balances of investment and satisfaction values are equilibrated for the successive exchanges occurring along the time. A (centralized) mechanism for the regulation of social exchanges in MAS, based on the concept of equilibrium supervisor with an associated Qualitative Interval Markov Decision Process (QI-MDP) was introduced in 2005. This approach was extended to consider personality-based agents in 2006.
We are now going towards the (distributed) self-regulation of personality-based social exchanges, by decentralizing the equilibrium supervisor through the internalization of its decision process in the interacting agents. For simplicity, we consider that the exchanges between each pair of agents have no influence from the exchanges occurring between other pair of agents, which allowed for a simple way of distributing the decision process. However, since the agents do not necessarily have access to the internal states (balances of exchange values) of each other, the decision processes have to operate in a partially observable mode, by means of Partially Observable Markov Models POMDP).
The decision about the best exchanges that an agent should propose to its partner in order to achieve social equilibrium, or to promote new interactions, is modeled as a global POMDP for each personality trait that its partner may assume. Considering a set of six personality traits (egoism, strong egoism, altruism, strong altruism, tolerance, equilibrium fanaticism), each global POMDP is decomposed into three sub-POMDPs, according to the current internal state (favorable, equilibrated or unfavorable balance of material exchange values) of the agent that is supervising the interaction.
For convenience, we have chosen the BDI architecture for the agents in the social exchange simulator used in this work. We developed an algorithm to extract BDI plans from the policy graphs of each sub-POMDP, building a set of rules that form the BDI plans for interacting with agents of each personality model. Those plans are to be selected in each interaction according to the current balance of material values of the agents in each exchange stage. Such plans are said to ``obey'' optimal POMDP policies.
quarta-feira, 24 de setembro de 2008
LÓGICAS DA INCONSISTÊNCIA DEÔNTICA
---------- Forwarded message ----------
From: Rafael Testa (CLE-UNICAMP)
![]()
LOCAL: CLE - UNICAMPLembro a todos que na próxima quarta, dia 1 de outubro, às 16h00, teremos seminário de nosso colega Newton Perón (Mestrando IFCH/CLE), cujo resumo segue abaixo.
Abraços,
Rafael
++++++++++++++++++++++++++++++++++++++++++++++++++++
LÓGICAS DA INCONSISTÊNCIA DEÔNTICA
resumo
Lógicas da Inconsistência Formal (LFI's). são lógicas que não trivializam na presença de contradições, pois a partir de A e ~A temos simplesmente que ~oA, ou seja, A não é consistente, ou não é seguro.
De mandeira análoga, as Lógicas da Inconsistência Deôntica (LDI's) são lógicas que não trivializam na presença de obrigações conflitantes, como OA e O~A. Nesse caso teríamos apenas [X]A, ou seja, A é deonticamente inconsistente, ou deonticamente inseguro. Exemplos de LDI's são os sistemas DmbC e BDmbC - esse último com dois operadores deônticos -, que serão apresentados. Já SDmbC é uma LFI deôntica que não pode ser classificada como LDI.
Essa abordagem torna-se interessante sobretudo na análise de paradoxos que, a partir de um conjunto de premissas, inferemos OA e O~A. Trataremos, como exemplo, a análise d'O Paradoxo de Chisholm.
__._,_.___ Abraços,
Rafael
++++++++++++++++++++++++++++++++++++++++++++++++++++
LÓGICAS DA INCONSISTÊNCIA DEÔNTICA
resumo
Lógicas da Inconsistência Formal (LFI's). são lógicas que não trivializam na presença de contradições, pois a partir de A e ~A temos simplesmente que ~oA, ou seja, A não é consistente, ou não é seguro.
De mandeira análoga, as Lógicas da Inconsistência Deôntica (LDI's) são lógicas que não trivializam na presença de obrigações conflitantes, como OA e O~A. Nesse caso teríamos apenas [X]A, ou seja, A é deonticamente inconsistente, ou deonticamente inseguro. Exemplos de LDI's são os sistemas DmbC e BDmbC - esse último com dois operadores deônticos -, que serão apresentados. Já SDmbC é uma LFI deôntica que não pode ser classificada como LDI.
Essa abordagem torna-se interessante sobretudo na análise de paradoxos que, a partir de um conjunto de premissas, inferemos OA e O~A. Trataremos, como exemplo, a análise d'O Paradoxo de Chisholm.
segunda-feira, 22 de setembro de 2008
Verdade: mito e demito
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:
Verdade: mito e demito
Prof. Abrahão Costa Andrade
Departamento de Filosofia - UFPB
Data: 26/09/2008 às 16 h.
Local: UFRN, Setor II, sala D1
Verdade: mito e demito
Prof. Abrahão Costa Andrade
Departamento de Filosofia - UFPB
Data: 26/09/2008 às 16 h.
Local: UFRN, Setor II, sala D1
sexta-feira, 19 de setembro de 2008
A Conferência KR 2008 (Knowledge Representation) - Seminário LIAMF dia 22/09
-----------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: A Conferência KR 2008 (Knowledge Representation)
Palestrante: Renata Wasssermann e Leliane Barros
Resumo:
A Conferência KR é o maior evento internacional da área de representação de
conhecimento, e a Renata e Leliane estiveram presentes a edição de 2008 na
Austrália e vão contar o que viram por lá, quais os assuntos que estão na moda,
quais os resultados mais notáveis e como seus trabalhos foram recebidos.
Todos são benvindos.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
Seminário LIAMF 15/09/2008
-----------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: Using Abduction to Compute Efficient Proofs
Palestrante: Marcelo Finger
Data: 15/09/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
--------------
The aim of this work is to present a solution to the problem
of computing non-analytic cuts. Several algorithms are
provided that compute efficient proofs with non-analytic
cuts via extended abductive reasoning.
Extended abductive reasoning computes an extra hypothesis
to a statement whose validity is unknown, such that:
-- The statement becomes provable with the addition
of the extra hypothesis.
-- The extra hypothesis is not trivial (in some precisely
defined sense).
-- If the statement was originally valid (which is not known a priory)
then the addition of the extra hypothesis leads to a statement
with a much simpler proof.
Due to the last item, this is ***not exactly*** the usual abductive
reasoning found in literature, for the latter requires the input
to be invalid.
The idea is that the input is a contextual database, containing
background knowledge, plus a goal formula representing some fact
or evidence that one wants to explain or prove, and we want to
compute an hypothesis that explains the evidence in the presence
of the background knowledge or that facilitates the proof of
$G$ from $\Gamma$.
This is a joint work with Marcello D'Agostina and Dov Gabbay.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------
Título: Using Abduction to Compute Efficient Proofs
Palestrante: Marcelo Finger
Data: 15/09/2008, 14h30
Local: Sala 03B, IME-USP
Resumo:
--------------
The aim of this work is to present a solution to the problem
of computing non-analytic cuts. Several algorithms are
provided that compute efficient proofs with non-analytic
cuts via extended abductive reasoning.
Extended abductive reasoning computes an extra hypothesis
to a statement whose validity is unknown, such that:
-- The statement becomes provable with the addition
of the extra hypothesis.
-- The extra hypothesis is not trivial (in some precisely
defined sense).
-- If the statement was originally valid (which is not known a priory)
then the addition of the extra hypothesis leads to a statement
with a much simpler proof.
Due to the last item, this is ***not exactly*** the usual abductive
reasoning found in literature, for the latter requires the input
to be invalid.
The idea is that the input is a contextual database, containing
background knowledge, plus a goal formula representing some fact
or evidence that one wants to explain or prove, and we want to
compute an hypothesis that explains the evidence in the presence
of the background knowledge or that facilitates the proof of
$G$ from $\Gamma$.
This is a joint work with Marcello D'Agostina and Dov Gabbay.
--
Marcelo Finger
Departamento de Ciencia da Computacao
Instituto de Matematica e Estatistica | home page:
Universidade de Sao Paulo | www.ime.usp.br/~mfinger
Rua do Matao, 1010 | Tel: +55 11 3091 6310, 3091 6135
05508-090 Sao Paulo, SP Brazil | Fax: +55 11 3091 6134, 3814 4135
quinta-feira, 21 de agosto de 2008
O conceito de verdade nas línguas naturais
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
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
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
Assinar:
Postagens (Atom)