Everton Guerra Marques
Roteiro
 Introdução à lógica Modal
 Saul Kripke
 Lógica modal K
 Lógica de Descrição x Lógica modal K
 Conclusão
 Referências
Introdução à lógica modal
 Principais contribuidores da lógica modal
 Clarence Irving Lewis - em 1912 deu origem a lógica moderna,
composta pelas três tradições: semântica, algébrica e
sintática.
 Saul Aaron Kripke - amplamente conhecido como um dos
mais importantes filósofos vivos. Publicou Semantical
Considerations on Modal Logic em 1963, onde propôs uma
resposta a uma dificuldade da teoria clássica da quantificação.
 Amir Pnueli - primeiro utilizador da lógica temporal.
 Vaughan Ronald Pratt - desenvolvedor do sistema de lógica
dinâmica
 Arthur Norman Prior - fundou a lógica temporal e contribuiu
com a lógica intencional.
Introdução à lógica modal
 A Lógica Modal faz parte da pesquisa atual em diversas
áreas da ciência da computação.
 Encontram-se algumas aplicações na área de:
 Inteligência artificial
 Representação do conhecimento e dedução automática
 Especificação formal de sistemas
 Engenharia de software e lingüística computacional.
Introdução à lógica modal
 A Lógica Modal pode ser encarada como uma extensão
da Lógica Proposicional.
 Grande parte das lógicas modais teve origem em uma
lógica "fraca", conhecida como Lógica K.
 A lógica K leva este nome em homenagem a Saul
Kripke por sua contribuição.
 A Lógica Modal é bastante utilizada na análise
semântica, visto que as representações dos conectivos
modais permitem expressar advérbios, dentre os quais
a Lógica Clássica não pode representar.
Introdução à lógica modal
 Uma compreensão da Lógica Modal é particularmente
valiosa na análise formal de argumento filosófico onde
expressões da família modal são comuns e confusas.
 Trata-se da lógica do "é necessário que" (representado
por “") e do é "possível que" (representado por “◊”).
 Portanto, não considera apenas a veracidade e a
falsidade das proposições como se apresentam, mas
como seria se fossem diferentes.
Introdução à lógica modal
 Como um operador pode ser derivado do outro, pode-
se manter uma representação de apenas um deles e
fazer uma transformação na expressão trabalhada
sempre que se encontra o outro.
 Há algumas variações de lógica modal, dependendo de
quais axiomas são incluídos no conjunto de axiomas
básicos (da lógica proposicional).
Introdução à lógica modal
 Há outros operadores lógicos que podem ser derivados
dos já definidos (os quatro da lógica proposicional,
mas os dois acima citados).
 Por exemplo, o 'ou-exclusivo'. Apesar de não ter uma
notação padrão, é comum representá-lo por f1 f2 .
 A regra do ou-exclusivo é se duas fórmulas f1 e f2 são
ambas verdadeiras ou ambas falsas, f1 f2 é falsa. Caso
contrário é verdadeiro.
Introdução à lógica modal
 Esta lógica permite analisar não só o que dizem as coisas no
mundo, mas o que diriam em um mundo alternativo; não
factual, mas possível.
 Isto é, se interessa pelas verdades e falsidades que são
geradas por asserções neste mundo real e em outros
possíveis mundos, visto que se chama de mundo possível
uma situação contra-fatual que não aconteceu, mas poderia
ter acontecido.
 Neste sentido, uma proposição será necessária em um
mundo se ela é verdadeira em todos os possíveis mundos
relacionados com este, e possível em um mundo se essa é
verdadeira em pelo menos um daqueles mundos
relacionados a este.
Introdução à lógica modal
 Lógicas modais tratam de modalidades. Além dos
conectivos são inseridos dois novos conectivos unários
(modalidades):
Introdução à lógica modal
 Linguagem das lógicas modais:
 Alfabeto: Símbolos lógicos, e símbolos proposicionais
(P).
 Linguagem:
é menor conjunto que:




então
então
então
com
Introdução à lógica modal
 Aplicações
 Solução de problemas de sentenças proposicionais
 Análise formal de argumento filosófico
 Estudo da inteligência artificial
Saul Kripke
 Saul Aaron Kripke:
 nascido em 1940 em Omaha, Nebraska.
 É amplamente reconhecido como um dos filósofos vivos
mais importantes. Sua obra é muito influente em
diversas áreas da filosofia, desde a lógica até a filosofia
da mente, passando pela filosofia da linguagem.
 Ele é professor emérito em Princeton e professor de
filosofia na City University of New York (CUNY).
 Boa parte da sua obra é inédita, e circula na forma de
gravações de áudio e cópias de manuscritos. Em 2001 ele
recebeu o Prêmio Schock em Lógica e Filosofia.
Saul Kripke
 Kripke
é conhecido principalmente por quatro
contribuições para a filosofia:
 uma semântica para a lógica modal e outras lógicas
relacionadas, publicadas quando ele tinha menos de
vinte anos de idade;
 suas conferências Naming and necessity, proferidas em
Princeton em 1970 (publicadas em 1972 e 1980);
 uma interpretação controversa de Wittgenstein;
 sua teoria da verdade;
Saul Kripke
 Dois
dos primeiros trabalhos de Kripke (A
Completeness
Theorem
in
Modal
Logic
e
Considerations on Modal Logic) influenciaram
amplamente a lógica modal.
 Em Semantical Considerations on Modal Logic,
publicado em 1963, Kripke responde a uma dificuldade
da teoria clássica da quantificação.
 Toda a motivação para a abordagem relativa a mundos
era refletir a idéia que objetos existentes em um
mundo podem não existir em outro.
Saul Kripke
 Todavia, se as regras de quantificação padrão são utilizadas,
cada termo deve referir a algo que existe em todos os
mundos possíveis.
 Isso parece incompatível com nossa prática comum de usar
termos para nos referirmos a coisas que existem apenas
contigentemente, não necessariamente.
 A resposta de Kripke a essa dificuldade foi eliminar termos.
Ele deu um exemplo de uma interpretação relativa a um
mundo que preserva as regras clássicas.
 Todavia, o custo para a solução do problema foi caro.
Primeiro, sua linguagem foi empobrecida artificialmente.
Segundo, as regras para a lógica modal proposicional
devem ser enfraquecidas.
Lógica Modal K
 Grande parte das lógicas modais teve origem em uma
lógica "fraca", conhecida como Lógica K, que leva este
nome em homenagem a Saul Kripke por sua contribuição.
 Um modelo de Kripke é uma tripla m = <Wm,Rm,hm> tal
que:
 Wm é um conjunto não vazio dos mundos possíveis de m;
 Rm C Wm x Wm representa a relação de acessibilidade de m;
 hm : ν → ρ(Wm) é uma função que estabelece um valor de
verdade arbitrário para cada fórmula atômica da linguagem e
um valor para cada fórmula molecular em vista dos valores
das fórmulas atômicas.
Lógica Modal K
 Axiomatização da Lógica Modal Normal Mínima (K)
 Primeiramente definiremos a sintática da lógica modal
por sua axiomática. Existem vários tipos de lógica
modal, começaremos descrevendo a axiomática da
menor lógica normal, também chamada de lógica K:
 Axiomas


A0) Todas as tautologias clássicas
K)
Lógica Modal K
 Regras de Inferência

Modus Ponens:

Necessitação:

Obs.: Para podermos derivar
não é sempre verdade que
temos que ter provado A,
Lógica modal K
 Estrutura de Krypke
 Uma estrutura (frame)de Krypke é um par (W,R)
onde:


W é um conjunto não vazio. Representa o conjunto de
mundos possíveis
é uma relação binária. Relação de acessibilidade.
 Modelo de Krypke
 μ = (W,R,v) é um modelo de Krypke se e somente se:

(W,R) é uma estrutura de Krypke. Ou seja v leva símbolos
proposicionais aos mundos nos quais eles são verdadeiros.
Lógica modal K
 No exemplo da figura 1 o conjunto de estados é W =
{s1;s2; s3; s4; s5} e a relação de acessibilidade é R = {(s1;
s2); (s1; s3); (s3; s3); (s3; s4); (s2; s4); (s2; s5);(s4; s1);
(s4; s5); (s5; s5)g. O frame é F = (W;R).
Lógica Modal K
 No exemplo da figura 2 o frame é o mesmo da figura 1 e
a função V é:
 V (p) = {s3; s4; s5}
 V (q) = {s1; s5}
 V (r) = {s1}
Lógica modal K
 Uma semântica de Kripke, ou sistema modal, é uma
classe Kr de modelos de Kripke.
 O sistema K é o menor dos sistemas modais normais,
isto é, a interseção de todos os sistemas modais
normais, justificado pelos seguintes princípios:
 se trata de um sistema de lógica modal, visto que se trata
de um conjunto de axiomas e regras de inferência que
representam formalmente o raciocínio válido;
 é fechado para modus ponens e necessitação, isto é, se A
é uma tese então  A é uma tese;
Lógica modal K
 contém os axiomas K e Df ◊:
 K: ((A → B)) →(( A) → ( B));
 Df◊: (◊ A) ↔ (¬( ¬A));
 Uma assinatura é uma família C = {Cn}{n∈N} tal que
cada Cn é um conjunto, sendo que Cn ∩ Cm = ø se n ≠
m. Os elementos do conjunto Cn são chamados
conectivos n-ários. Em particular, os elementos de C0
são chamados constantes. O domínio de C é o conjunto
|C| = ∪{Cn : Cn ∈ N }
Lógica modal K
 Uma assinatura modal é uma assinatura C tal que C1 =
{¬,◊, ,}; C2 = {→,↔,∧,∨}; Cn = ø se n ≠ 1, n ≠ 2.
 É importante observar que a relação de conseqüência
de uma lógica modal pode ser obtida a partir de
diferentes semânticas de Kripke.
Lógica de Descrição X Lógica Modal K
 Lógica de Descrição
 Descende das redes de heranças estruturadas
 Tentou resolver ambigüidades em redes semânticas e frames
que eram herança da falta de uma semântica formal.
 Restrição a um pequeno conjunto de operadores
“adequadamente epistemológicos” para conceitos definidos
(Classes).
 Importância de procedimentos de inferência básicos bem
definidos.
 Primeira implementação: KL-ONE.
 Primeira aplicação: Processamento de linguagens naturais.
Agora é aplicado em outros domínios.
Lógica de Descrição X Lógica Modal K
 Família
de formalismos de representação de
conhecimento baseado em lógica apropriada para
“representação de” e “explicação sobre”:
 Conhecimento terminológico
 Configurações
 Ontologias
 Esquema de Banco de Dados
Lógica de Descrição X Lógica Modal K
 Sistemas de Lógicas de Descrição - Arquitetura
Lógica de Descrição X Lógica Modal K
 Sistemas de lógicas de Descrição - Arquitetura
Lógica de Descrição X Lógica Modal K
 Linguagem de descrição (DL ALC)
Lógica de Descrição X Lógica Modal K
 Uma lógica de descrição (DL ALC)
 Comumente caracterizada por um conjunto de construtores
que permitem a construção de conceitos e papéis complexos
através de itens atômicos
 Conceitos correspondem a classes / São interpretados como
um conjunto de objetos
 Papéis correspondem a relações / São interpretados como
relações binárias sobre objetos
 Exemplo: Pai feliz em DL ALC
Lógica de Descrição X Lógica Modal K
 Semântica formal – Baseado em interpretação assim
como em predicados lógicos
Lógica de Descrição X Lógica Modal K
 Sintaxe e Semântica de ALC
 Semântica dada por significados de uma interpretação
Lógica de Descrição X Lógica Modal K
 Antigamente, lógicas de descrição não pareciam ser
nada mais do que uma notação para falar sobre
conhecimento estruturado.
 Mas como elas foram equipadas com uma sintaxe e
semântica próprias, modelos e teorias de prova, em
resumo, tornaram-se uma lógica,e tornou-se possível
relacionar lógicas de descrição com outras áreas da
lógica.
 Em particular, a conexão entre lógicas de descrição de
um lado e lógicas modais do outro lado receberam
atenção especial.
Lógica de Descrição X Lógica Modal K
 Schild (1991) foi o primeiro a fazer explicitamente a
conexão entre a lógica de descrição e a lógica modal.
 Ele desenvolveu a correspondência entre lógicas de
descrição e lógicas dinâmicas proposicionais, que são
lógicas desenvolvidas para raciocínio sobre programas.
 Posteriormente Schild e De Giacomo e Lenzerini
identificaram a correspondência entre lógicas de
descrição e a lógica multi-modal K.
 A seguir, segue o mapeamento entre lógica de
descrição e a lógica modal K.
Lógica de Descrição X Lógica Modal K
 Mapeamento entre ALC e Lógica Modal K
Lógica de Descrição X Lógica Modal K
 Mapeamento entre ALC e Lógica Modal K
Conclusão
 Schild (1991) mostrou que algumas lógicas de
descrição são variantes notacionais de certas lógicas
modais.
 Especificamente a DL ALC tem uma contra-parte na
lógica modal, chamada de versão multi-modal da
lógica K.
 Atualmente conceitos ALC e fórmulas em multi-modal
K podem imediatamente serem traduzidas de uma
para outra.
 Além disso, um conceito ALC é satisfatível se e
somente se a fórmula K correspondente for satisfatível.
Conclusão
 Pesquisas sobre a complexidade do problema da
satisfatibilidade para lógicas proposicionais modais
foram iniciadas pouco tempo antes da complexidade
das lógicas de descrição ser investigada.
 Conseqüentemente, essa relação tornou possível pegar
emprestado da lógica modal resultados complexos,
técnicas de raciocínio e construtores de linguagens que
não eram considerados anteriormente em Lógicas de
Descrição.
Conclusão
 Por outro lado, existem características da lógica de
descrição, que não tiveram contrapartidas na lógica
modal e, portanto,tornaram-se necessárias extensões
ad hoc das técnicas de raciocínio desenvolvias para a
lógica modal.
 Em particular, restrições de números, bem como o
tratamento de indivíduos no ABox, exigiram
tratamentos específicos baseado na idéia de reificação,
o que equivale a expressar as extensões através de um
tipo especial de axioma dentro da lógica.
Referências
 Wikipédia – Lógica modal
 http://pt.wikipedia.org/wiki/L%C3%B3gica_modal
 Wikipédia – Saul Kripke
 http://pt.wikipedia.org/wiki/Saul_Kripke
 Lógica formal – Meu TG
 http://www.cin.ufpe.br/~tg/2007-2/egm2.pdf
 Modal Logics And Description Logics
 Rijke, M. Modal Logics And Description Logics. IILC,
University of Amsterdam
Referências
 An Overview of Tableau Algorithms for Description Logics
 Baader, F.; Sattler, U. An Overview of Tableau Algorithms for
Description Logics. LuFG Theoretical Computer Science,
RWTH Aachen, Germany
 An Introduction to Description Logics
 Nardi, D. ; Branchman, R. An Introduction to Description
Logics.
 Nonstandard Inferences in Description Logics
 Baader, F. Nonstandard Inferences in Description Logics.
Theoretical Computer Science. RWTH Aachen.
Germany.Workshop
Referências
 Description logic
 Baader, F.; Cartzen, L. Description logic. E-book
 Description Logics - Basics, Applications, and More
 Horrocks, I. Description Logics-Basics, Applications, and
More. Information Management Group. University of
Manchester, UK. Workshop
 Tableau Algorithms for Description Logics
 Baader, F. Tableau Algorithms for Description Logics.
Theoretical Computer Science. RWTH Aachen.
Germany.Workshop