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



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.

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


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





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
==================================

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





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