terça-feira, 28 de abril de 2009

Uma abordagem lógico-social do fenômeno da incompletude


Quarta-feira, dia 29 de abril de 2009, 16h
Local: auditório do CLE, IFCH, UNICAMP


_______________________________________________________________

Título: Uma abordagem lógico-social do fenômeno da incompletude

Resumo: Daqui alguns anos, a prova de Gödel de seus dois famosos teoremas da incompletude completará cem anos. Em virtude do grande impacto desses resultados para a compreensão dos fundamentos da matemática, grande volume de pesquisa desenvolveu-se durante esse tempo, gerando o que podemos chamar de "fenômeno da incompletude". Não obstante a essa produção volumosa acerca do fênomeno da incompletude, algumas questões relativas à incompletude da aritmética ainda permanecem por serem plenamente tematizadas. Nesse contexto, pretendo apresentar o que chamo de uma "abordagem lógico-social" da aritmética e, por consequinte, do fenômeno da incompletude. Intuitivamente, essa abordagem trata a aritmética enquanto feita por agentes aritméticos. Tecnicamente, ela consiste da formulação de estruturas lógicas, chamadas "sociedades aritméticas", que combinam intuições e ferramentas da semântica de sociedades, por um lado, e da lógica da demonstrabilidade, por outro. As principais definições bem como os resultados em desenvolvimento no presente estágio de minha pesquisa serão apresentados neste seminário.

Apresentador: Anderson de Araújo
_____________________________________________________________



Revisão de Crenças em Lógica de Horn e Outros Fragmentos


------------------------------------------------------------------------------------------
 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: Revisão de Crenças em Lógica de Horn e Outros Fragmentos
Palestrante:  Renata Wassermann

Data:   30/04/2009, 14h00
Local:  Sala 241A, IME-USP

Resumo:
--------------
A teoria clássica de revisão de crenças, conhecida como teoria AGM
graças aos trabalhos iniciais de Alchourrón, Gärdenfors e Makinson,
geralmente assume que a lógica por trás do raciocínio do agente contém
no mínimo a lógica clássica. No entanto, nos últimos anos surgiu um
grande interesse por aplicações de revisão de crenças a lógicas
sub-clássicas, como a lógica de Horn e as lógicas de descrição. Neste
seminário pretendo apresentar os problemas que surgem quando abandonamos
a supraclassicalidade e algumas tentativas minhas e de outros de
solucioná-los.

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 9688, 3091
6135
 05508-090    Sao Paulo, SP     Brazil | Fax: +55 11 3091 6134, 3814
4135


quinta-feira, 23 de abril de 2009

Next Steps in Propositional Horn Contraction



Amanhã teremos a visita do Ivan Varzinczak, que foi aluno de doutorado do
Andreas Herzig em Toulouse e atualmente trabalha no Instituto Meraka, na África
do Sul. Faremos um seminário extra às 11:30, na sala de reuniões do bloco C.
Seguem os dados abaixo.


------------------------------------------------------------------------------------------
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: Next Steps in Propositional Horn Contraction

Palestrante: Ivan J. Varzinczak

Data:   23/04/2009, 11h30
Local:  Sala de reuniões, bloco C, IME-USP


Abstract: Standard belief contraction assumes an underlying logic containing
full classical propositional logic, but there are good reasons for considering
contraction in less expressive logics. In this paper we focus on Horn logic. In
addition to being of interest in its own right, our choice is motivated by the
use of Horn logic in several areas, including ontology reasoning in description
logics. We consider three versions of contraction: entailment-based and
inconsistency-based contraction (e-contraction and i-contraction, resp.),
introduced by Delgrande for Horn logic, and package contraction (p-contraction),
studied by Fuhrmann and Hansson for the classical case. We show that the
standard basic form of contraction, partial meet, is too strong in the Horn
case. We define more appropriate notions of basic contraction for all three
types above, and provide associated representation results in terms of
postulates. Our results stand in contrast to Delgrande's conjectures that
orderly maxichoice is the appropriate contraction for both e- and i-contraction.
Our interest in p-contraction stems from its relationship with an important
reasoning task in ontological reasoning: repairing the subsumption hierarchy in
EL. This is closely related to p-contraction with sets of basic Horn clauses
(Horn clauses of the form p -> q). We show that this restricted version of
p-contraction can also be represented as i-contraction.

Todos são benvindos.


O Algoritmo de Dubois e a transição de fase


-----------------------------------------------------------------------------
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:O Algoritmo de Dubois e a transição de fase
Palestrante: Eduardo Menezes

Data:   23/04/2009, 14h00
Local:  Sala 241A, IME-USP

A transição de fase no problema da satisfatibilidade booleana (SAT)  é um
fenômeno que afeta a maioria dos algoritmos utilizados hoje em dia e dificulta
muito o problema SAT para um certo intervalo de instâncias.
Neste seminário, será apresentado um algoritmo criado em 1989 por Olivier
Dubois. Esse algoritmo possui uma propriedade interessante: parece não sofrer
alteração no comportamento quando está na região da transição de fase.
Também serão apresentados idéia de otimizações que podem ser aplicadas ao
algoritmo de Dubois na tentativa de torná-lo mais competitivo em comparação com
os algoritmos atuais.
--
 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, 16 de abril de 2009

Classes de Complexidade de Linguagens


==========================================
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: Rafael Testa <rafaeltesta@gmail.com>
Date: 2009/4/16
Subject: [seminarios-CLE] seminário
To: seminarios-CLE@yahoogroups.com
Prezados,
lembro que próxima quarta, dia 22, teremos seminário do Prof. José Guimarães - como sempre às 16h00, no CLE. Título e resumo abaixo.
Contamos com a presença de todos.
Abraços,
Rafael Testa

+++++++++++++++++++++++++++=

Título: Classes de Complexidade de Linguagens
Resumo:
    Uma linguagem formal pode ser classificada de acordo com a complexidade das máquinas de Turing que podem decidir se um elemento pertence ou não a ela. As medidas de complexidade mais comuns são tempo e espaço. As linguagens formais podem ser agrupadas em classes de complexidade, que são conjuntos que contém linguagens com características de complexidade comum. Por exemplo, temos a class P das linguagens que podem ser decididas por uma máquina de Turing em um número de passos Polinomial no tamanho da entrada. E a classe NP das linguagens que podem ser aceitas por uma máquina de Turing não-determinística em tempo polinomial.
     Este seminário apresentará os teoremas básicos desta área de pesquisa e também os relacionamentos entre as mais importantes classes de complexidade, que são P, NP, PSPACE, NPSPACE e EXP. Finalizaremos apresentando uma sugestão de pesquisa nesta área.
   
José de Oliveira Guimarães é Professor da UFSCar desde 1992, atualmente no Campus de Sorocaba, tendo feito graduação, mestrado e doutorado em Computação. Suas áreas de atuação em pesquisa são Linguagens de Programação, Programação Orientada a Objetos, Reflexão Computacional e Compiladores. Suas áreas de interesse são Lógica (principalmente Computabilidade), Classes de Complexidade e Computação Quântica.



__._,_.___


KEMS - Um provador de teoremas multi-estratégia


Programação do 1º semestre de 2009:

http://www.dainf.ct.utfpr.edu.br/wiki/index.php/Semin%C3%A1rios_de_Pesquisa_do_DAINF

SÉRIE DE SEMINÁRIOS DE PESQUISA DO DAINF

             ***** 2ª PALESTRA *****

            DAINF - UTFPR

Data:   22 DE ABRIL de 2009, QUARTA-FEIRA
Hora:  10:30h
Local: Mini-Auditório da UTFPR - Campus Curitiba

Palestrante:
Prof. Adolfo Neto (DAINF-UTFPR)

Titulo: "
KEMS - Um provador de teoremas multi-estratégia"

Resumo: O KEMS (http://www.dainf.ct.utfpr.edu.br/~adolfo/KEMS) é um provador de teoremas multi-estratégia baseado no método KE. O sistema KE é um método de tablôs que foi apresentado como uma melhoria, no sentido da eficiência computacional, em relação ao método dos Tablôs Analíticos. Um provador de teoremas multi-estratrégia é um provador de teoremas no qual podemos variar a estratégia sem modificar o núcleo da implementação. Um provador de teoremas multi-estratégia pode ser utilizado com três propósitos: educacional, exploratório e adaptativo. Para fins educacionais, o KEMS pode ser usado para ilustrar como a escolha da estratégia de prova pode afetar a performance de um provador de teoremas. Como uma ferramenta exploratória, um provador de teoremas multi-estratégia pode ser usado para testar novas estratégias e compará-las com outras existentes. E podemos pensar também em um provador de teoremas multi-estratégia adaptativo que modifique a estratégia usada de acordo com as características do problema apresentado ao provador. O KEMS foi implementado durante o doutorado de Adolfo Neto, que foi orientado por Marcelo Finger. Nesta palestra discutiremos as contribuições do KEMS na área de Lógica para Computação. Falaremos também um pouco sobre a implementação do KEMS, que foi feita em Java e AspectJ (uma linguagem orientada a aspectos), usando algumas técnicas usadas em métodos ágeis de desenvolvimento de software.

Mini-CV: Adolfo Neto é Doutor em Ciências da Computação pela Universidade de São Paulo (USP), Mestre em Ciência da Computação pela Universidade Federal de Pernambuco (UFPE) e bacharel em Ciências da Computação pela Universidade Federal de Alagoas (UFAL). Atualmente é professor do Departamento de Informática (DAINF) da Universidade Tecnológica Federal do Paraná (UTFPR), Campus Curitiba. Foi professor da Universidade do Estado de Santa Catarina (UDESC), do Centro Federal de Educação Tecnológica de São Paulo (CEFET-SP), da Pontifícia Universidade Católica de Campinas (PUC-CAMPINAS), do Centro Federal de Educação Tecnológica de Alagoas (CEFET-AL) e da Universidade Federal de Alagoas. Foi analista desenvolvedor de sistemas na Inmetrics, uma empresa de soluções em serviços de APM.

Tem experiência na área de Ciência da Computação, com ênfase em Lógica Aplicada à Computação, atuando principalmente nos seguintes temas: sistemas de prova baseados em tablôs, prova automática de teoremas, e lógicas paraconsistentes. Tem, também, interesse em métodos ágeis para o desenvolvimento de software.



Todos são bem-vindos!!!


terça-feira, 14 de abril de 2009

Argumentation as a Methodology to Reason over Inconsistency

------------------------------------------------------------------------------------------
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: "Argumentation as a Methodology to Reason over Inconsistency"

Palestrante: Martin Moguillansky

Data:   16/04/2009, 14h00
Local:  Sala 241A, IME-USP

Resumo:

Since early times of ancient Greece, argumentation theory has been
applied to different areas of science. From philosophy, passing through
law, to civil dialogue; in the last decades argumentation has being
theorized into a practical approach, gaining the attention of computer
scientists. Specifically, in artificial intelligence, argumentation has
being applied with the objective of reasoning about non-monotonic
logics.

Argumentative reasoning methodologies are devoted to the decision of
which arguments should prevail from a potentially conflicting
environment. Bridging the frontiers of philosophy to knowledge
representation, argumentation may provide a powerful methodology to
reason about inconsistent knowledge bases. In consequence, novel
approaches of knowledge base change arise as one of the promissory
results.



Todos são benvindos!!!

segunda-feira, 13 de abril de 2009

Workshop Negação - PROGRAMAÇÃO

-------------------------------------------------------
WORKSHOP - ASPECTOS LÓGICOS DA NEGAÇÃO
20 e 21 de Abril de 2009
Natal-RN - Departamento de Filosofia
-------------------------------------------------------

PROGRAMA

SEGUNDA - 20/04
09:00 (Frank Sautter) - Silogísticas Paraclássicas.
10:00 (Patrick Terrematte) - Princípio de Prova Indireta e Relações
Positivas em Dedução Natural.
11:00 (João Marcos) - Simulating Negtation in Positive Logic
14:00 - Sessão de Discussão.

TERÇA - 21/04
09:00 (Wagner Sanz) - Contrariedade, Contradição e Negação
10:00 (Abilio Rodrigues) - Fazedores-de-Verdade e Proposições Negativas
11:00 (Daniel Durante) - O Projeto "Simulações Positivas da Negação"
14:00 - Sessão de Discussão.

RESUMOS

*Wagner Sanz - */Contrariedade, Contradição e Negação/

O comportamento lógico da negação nas linguagens naturais aparece de uma
forma exacerbadamente complexa. Quando nos restringimos oa comportamento
da negação no âmbito da linguagem matemática, sobretudo nas provas
matemáticas, seu comportamento é mais tratável, mas nem por isso as
questões e disputas são de menor complexidade. Desde um certo ponto de
vista, a diferença entre construtivistas e clássicos pode quase
inteiramente ser circunscrita ao âmbito da negação. Nosso objetivo no
workshop será o de apresentar algumas variantes para o tratamento da
negação usando os sistemas de dedução natural e procurar oferecer um
quadro conceitual compatível com esses tratamentos. Em particular,
seguindo a tradição construtivista, procurar dar substância a uma
distinção que nos parece fundamental: aquela entre problemas lógicos e
problemas extra-lógicos no uso da argumentação e das inferências. Como
se trata de um workshop, a idéia é de trazer temas elementares mais
elaborados mas também apresentar propostas para o debate.

*Frank Sautter - */Silogísticas Paraclássicas/

Sob a perspectiva peripatética, silogismos aristotélicos com termos
concretos não fazem parte da lógica. Sob essa perspectiva, a silogística
aristotélica não é paraconsistente. Construo duas silogísticas que,
respeitando a restrição peripatética, são paraconsitentes de tipo
paraclássico. Na construção dessas silogísticas recorro a duas idéias de
Nikolai Vasiliev: a utilização de juízos duplos e a obtenção de sistemas
completos de juízos opostos contrários entre si. Utilizo essas
silogísticas para mostrar e corrigir uma inadequação do método
diagramático proposto por John Venn. Obtenho, também, uma lógica
proposicional paraclássica ao utilizar as formas normais conjuntiva e
disjuntiva. Esses sistemas paraclássicos apóiam a tese geral de que a
maioria, senão todos, os sistemas lógicos não-clássicos resultam da
fusão da lógica clássica e elementos extralógicos.


*Abilio Rodirgues - */Fazedores-de-Verdade de Proposições Negativas/

A noção de fazedor-de-verdade (/truthmaker/) pretende capturar a tese
segundo a qual a verdade é ontologicamente fundada na realidade. A idéia
básica é expressada pelo esquema /p é verdadeira se, e somente se,
existe um s tal que s >/ /p/, no qual '/s >/ /p/' se lê '/s faz
verdadeira a proposição p/'. Mas o que seria o fazedor-de-verdade de um
existencial negativo como (1) /não existem pingüins no pólo norte/? É
consenso que estados de coisas negativos não são uma boa solução. Mas
soluções baseadas apenas em entidades positivas não são bem-sucedidas.
Uma alternativa é afirmar que um estado de coisas maximal, que
contivesse todos os estados de coisas positivos acerca de um mundo /w/
poderia cumprir o papel de fazedor-de-verdade para proposições
negativas. Assim, /w /> (1). Mas se um mundo /w /não for caracterizado
negativamente, como 'nada mais existe além de /w/', /w /pode ser uma
parte própria de um mundo /w/_/1/ tal que (1) é falsa em /w/_/1/ . Logo,
não é o caso que /w /> (1). Outra alternativa se baseia na chamada /tese
da incompatibilidade/: /p/ e /q/ são incompatíveis se, e somente se,
necessariamente(/p/ sse /~q/). Sendo /s/ > /p/, temos que /s/ > /~q/.
Mas surge a demanda por um fazedor-de-verdade para a incompatibilidade
entre /p /e /q /e estamos novamente diante do problema das proposições
existenciais negativas. O objetivo da minha comunicação é apresentar e
discutir esses problemas.


*João Marcos - */Simulating Negation in Positive Logic/

The first part of this talk will consider what happens when one adds a
new axiomless 0-ary constant to (propositional) positive logics,
providing conservative extensions of them into 'logics of assertibility
or refutability'. The second part will show that the resulting logics
are essentially *non-truth-functional*, and then consider what happens
when one adds axioms that forces this new constant to behave as the
supremum or as the infimum of the corresponding algebras of values. The
third part will evaluate the behavior and propose adequate formal
non-deterministic semantics for several unary constants defined with the
help of the above 0_ary constant, and show in which circumstances such
unary constants behave as *negations* or alternatively as *identity*
connectives. The final picture will display, among other things, the
relations that hold between the positive fragments of both
intuitionistic and classical logic, as well as Johánsson's minimal
intuitionistic logic, Curry's logic of classical refutability, full
intuitionistic logic and full classical logic, and also their
paracomplete relatives.


*Patrick Terrematte - */Princípio de Prova Indireta e Relações Positivas
em Dedução Natural/

Em uma perspectiva da dedução natural¹, assumindo uma prova de
Normalização (Seldin 1989²), apresentaremos uma demonstração de que a
partir de uma derivação positiva (sem negação) no Sistema Proposicional
Clássico, nós podemos convertê-la em uma derivação no Sistema Positivo
acrescido da regra Peirce. Trata-se de uma demonstração bastante
econômica conceitualmente, supondo essencialmente o conceito de
Princípio de Sub-fórmula, e demonstrando que podemos substituir para
qualquer derivação cada ocorrência de absurdo pela conjunção de todas as
fórmulas obtidas por regras de absurdo intuicionista. O objetivo desta
abordagem é esclarecer os limites do que ser demonstrado sem a negação.
Por fim, vamos propor um novo teorema ampliado para lógicas de ordens
superiores e analisaremos as implicações filosóficas destes resultados.


*Daniel Durante - */O Projeto "Simulações Positivas da Negação"/

Trata-se de um estudo filosófico sobre a negação cujas análises se
inserem na tradição lógica da Teoria da Prova. Investiga-se a
possibilidade de simular positivamente a negação em sistemas formais de
lógica e avaliar o sucesso e o caráter positivo destas simulações, com o
intuito de ampliar a compreensão da negação enquanto operação racional
passível de formalização. Busca-se compreender a negação mediante uma
análise dos efeitos de sua ausência nos sistemas lógicos, procurando
suprir ou minorar estes efeitos simulando-a por via de artifícios
formais supostamente positivos. Pretende-se que a comparação destes
sistemas 'positivos' com conhecidos sistemas de lógica intuicionista,
clássica, paraconsistentes e relevantes forneçam esclarecimentos sobre o
exato papel da negação nestes sistemas, enquanto ferramenta dedutiva.