Resumo do Artigo “Automated Reasoning”
Felipe S. Boffo
Fernando dos Santos
Leomar Costa
Leonardo Couto
Roger Reis
1/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
 (fi) = Uma conjectura, uma propriedade, uma sentença a
ser verificada
S = Conjunto de suposições que expressam propriedades de
um objeto de estudo (Exemplo: um sistema, circuito,
estrutura matemática, etc )
2/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
 é uma conseqüência lógica do conjunto S
de suposições ?
3/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Problema: representação do conhecimento
Formalismo adequado para S e  para
representar aspectos do mundo real como
ação, espaço, tempo, eventos mentais e
raciocínio de senso comum
4/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Lógica clássica: tem sido o principal formalismo em
raciocínio automático
Lógicas não clássicas: modal, temporal, descritiva e lógicas
não monolíticas
Lógicas não clássicas tem sido largamente investigadas
para representar conhecimento
5/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
1.2
Raciocínio Automático na Lógica Clássica
Teorema da Prova
O Problema e os métodos para demonstrar que uma
propriedade  é uma conseqüência lógica de S
6/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Teorema Dedutivo de Prova
Se interessa em provar que  é uma conseqüência lógica de
S (com os símbolos S ╞ )
Todo homem é mortal.
Sócrates é um homem.
Isto implica que Sócrates é mortal.
7/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Teorema Indutivo de Prova
Se interessa em determinar se S envolve todos os
fundamentos de  (em símbolos S ╞ ), onde 
representa todos os fundamentos
Este gelo é frio.
Uma bola de bilhar se move quando golpeada por um
taco.
Todo gelo é frio.
Toda bola de bilhar se move quando golpeada por8/64
um
taco.
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Teorema de prova automática
Uma máquina deve encontrar sozinha a prova
Teorema de prova interativa
A prova surge apartir da interação entre a máquina e um
humano.
9/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Muito difícil encontrar uma prova ignorando a conjectura
Maioria dos métodos de teorema de prova trabalham
refutacionalmente
Provam que  vem de S mostrando:
S U {} gera uma contradição ou é inconsistente.
10/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Ou provam que  é falso encontrando um contra exemplo
ou contra modelo
Um modelo onde S U {}
Este ramo do raciocínio automático é chamado construção
automática de modelos.
11/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Na lógica clássica de primeira ordem, o teorema dedutivo
de prova é Semi-decidível
Semi-decidível: é possível construir um algoritmo que pára
para determinados casos, mas não para para outros
12/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Teorema indutivo de prova não é nem mesmo semidecidíveis
Isto é significante porque enquanto existem vários livros
que falam sobre teorema de prova desde a década de 70, o
primeiro livro sobre construção de modelos surgiu
recentemente, em 2004
13/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
A maioria das abordagens de construção automática de
modelos combinam características destes três princípios:
1 - Método de enumeração: gera interpretações e testa
se eles são modelos de um dado conjunto de fórmulas;
14/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
2 - Método de saturação:
Extrai modelos de um conjunto finito de fórmulas geradas
por uma tentativa de refutação que falhou
15/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
3 - Métodos simultâneos:
pesquisam simultaneamente por uma refutação ou um
modelo de um dado conjunto de fórmulas
16/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Lógicas de maior ordem (,  )
Até mesmo teorema dedutivo de prova não são semidecidíveis.
Em função disto, o teorema de prova totalmente automática
foca no método dedutiva de prova.
Já introdução, geração de modelos e raciocínio em lógicas
de maior ordem recorrem à teoria de prova interativa.
17/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Como os mais importante recursos das lógicas de maior
ordem para a ciência da computação são funções de maior
ordem, que tem relação com as linguagens de programação
funcional ...
18/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Solução intermediária para lógicas de maior ordem:
Desenvolver um sistema de primeira ordem, que é uma
linguagem
de
programação
funcional,
usada
simultaneamente como linguagem de programação e como
linguagem lógica.
19/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Teorema de Prova Totalmente Automatizado
O melhor possível:
Algoritmo semi-decidível que para e retorna uma prova, se
S U {} é inconsistente.
Se ele para sem chegar há uma prova, nós podemos
concluir que S U {} é consistente e tentar extrair o
modelo da sua saída.
Porém, não é garantido que o procedimento pare quando a
situação for consistente.
20/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Existem finitas provas de inconsistência para S U {}, se
elas existem
Problema: espaço de pesquisa infinito de conseqüências
lógicas necessário percorrer para encontrar a contradição
Uma máquina deve realizar esta tarefa usando o mínimo de
recursos
21/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Idéia fundamental
É crucial a habilidade de reconhecer e descartar formulas
redundantes tanto quanto a capacidade de gerar
conseqüências para uma uma determinada fórmula.
22/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Adicionalmente as regras de inferência na forma
Que adiciona fórmulas inferidas b1 ... bm para o conjunto de
problemas conhecidos, que já inclui as premissas a1... an ...
23/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Sistemas de inferência contemporâneos possuem regras de
contração, que apaga ou simplifica teoremas já inferidos
É uma regra de exclusão se as conseqüências são um
subconjunto apropriado das premissas, caso contrário, é
uma regra de simplificação.
24/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Uma regra de expansão é quando o que é gerado é uma
conseqüência lógica das premissas
Exemplos: resolução(resolution) e (paramodulation).
{A1...An} ╞ { B1...Bn }
Um regra de contração é quando o que é removido é uma
conseqüência lógica do que está a esquerda ou adicionado
Exemplo: subsumption e equational simplification from
Knuth-Bendix completion.
25/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Um sistema de inferência é quando todas as regras são
refutacionalmente completas (refutationally complete), se
ela nos permite derivar uma contradição sempre que o
conjunto inicial de fórmulas é inconsistente.
26/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
O desafio é trabalhar com a contradição sem pôr em perigo
a integralidade.
A chave para isto é ordenar os dados (termos, literais,
clausulas, fórmulas, provas) de acordo com well-founded
orderings.
27/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Procedimentos de Decisão e SAT solvers
Exemplos decidíveis de problemas de raciocínio existem.
Para estes problemas, o espaço de pesquisa é finito e os
procedimentos de decisão são conhecidos.
28/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Decidibilidade pode parar de impor restrições:
;

na lógica;

na forma de admitir formulas para S ou

na teoria apresentada pela suposição de
S.
29/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
O exemplo mais relevante é a lógica proposicional, cujo
problema da satisfabilidade decidível é conhecido como
SAT.
Muitos problemas na ciência da computação podem ser
codificados dentro da lógica proposicional, reduzidos para
SAT e submetidos para SAT solvers, o paradigma
predominante é o procedimento DPLL.
30/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Decidível  prático
Problemas de raciocínio decidível são tipicamente NPcompletos
Raciocínio automático confia no paradigma de pesquisa da
inteligência artificial.
31/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Raciocínio automatizado como um problema de busca
Métodos de raciocínio automatizado são estratégias
compostas de:
- um sistema de inferência e
- um plano de busca
A forma de descrever estas estratégias não é óbvia e
diferentes formalismos capturam diferentes níveis de
abstração.
32/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Sistema de inferência
É um conjunto de regras de inferência não-determinístico
que define um espaço de busca com todas as possíveis
inferências.
U: Conjunto Universo contendo
todas as inferências possíveis.
S: Conjunto definido pelas regras
de inferência que definem o espaço
de busca.
33/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Plano de busca
O plano de busca guia o procedimento transformando um
sistema de inferência não-determinístico em procedimento
de prova determinístico.
34/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Plano de busca
Define, em qual etapa, qual regra de inferência usar e sobre
quais fórmulas.
Determina de forma única a escolha de regras de expansão
ou de contração sobre o conjunto de fórmulas.
São várias as estratégias que podem ser usadas.
35/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Estratégias
Estratégias baseadas em ordenação
Empregam uma well-founded ordering para permitir
restringir a expansão e definir a contração do
conjunto de fórmulas.
É esta ordenação que permite avançar ou recuar no
desenvolvimento da prova conforme a necessidade.
36/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Estratégias
Estratégias baseadas em contração
São estratégias baseadas em ordenação que
priorizam regras de contração para minimizar o
crescimento da base de fórmulas.
Podem usar simplificações ou generalizações.
37/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Estratégias
Raciocínio postergado
Estas estratégias trabalham com o chamado
raciocínio postergado, ou seja, não distinguem entre
cláusulas do objetivo de outras cláusulas.
Geram redundância por permitirem criar cláusulas
que nada acrescentam à prova
38/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Estratégias
Estratégias semânticas
Usam conjuntos de suporte ou estratégias orientadas
ao alvo para limitar este efeito.
39/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Estratégias
Redução a subobjetivos
Tratam do problema buscando soluções para
subproblemas do problema.
Incluem métodos como

Eliminação de modelo

Resolução linear

Matings

Connections
Que estão dentro do contexto das clausal
normalform tableaux.
40/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Estratégias
Estratégias baseadas em instância
Usam instâncias fixas das cláusulas a serem
refutadas.
Detectam inconsistências no nível proposicional
usando ferramentas SAT.
41/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Sistemas de raciocínio interativo
Sistemas de raciocínio interativo que tratam problemas de
ordem mais elevada que a proposicional também usam
estratégias de busca, mas de forma indireta ou através de
uma metalinguagem.
42/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Sistemas de raciocínio interativo
Uma sessão gera um plano de prova, isto é, uma seqüência
de ações para se chegar à prova.
As ações podem ser escolhidas pelo usuário ou pelo plano
de busca.
43/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Sistemas de raciocínio interativo
Ações




Aplicação de uma regra de inferência
Introdução de um lema
Invocação de um provador de primeira-ordem
para conjectura de primeira-ordem
Invocação de programa de decisão para um
subproblema decidível
44/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Aplicações
Apesar da dificuldade intrínseca, o raciocínio automatizado
é importante por várias razões.
Exemplos de aplicações diretas

Verificação de hardware/software

Geração de programas
45/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Aplicações
Provadores de teoremas foram aplicados com sucesso em

Verificação de protocolos criptográficos

Sistemas orientados a mensagens

Especificações de software
46/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Aplicações
As técnicas desenvolvidas contribuíram com outros campos
de IA como

Planejamento

Aprendizado

Processamento de linguagem natural

Computação simbólica
¤
Solução de problemas com restrições
¤
Álgebra de computador
47/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Aplicações
 Lógica computacional
¤
Programação declarativa
¤
Banco de dados dedutivos
 Matemática
¤
Banco de dados com verificação matemática
por computador
48/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Aplicações
Provadores de teorema são capazes de provar teoremas
matemáticos não triviais tais como teorias em

Álgebras Booleanas

Anéis

Grupos

Quasigrupos

Lógica multivalorada
49/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Aplicações
Deve-se destacar que o estudo de formas mecânicas de
raciocínio lógico é parte da questão fundamental,
particularizada pelo campo da Inteligência Artificial, sobre
o que uma máquina pode fazer.
.
50/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Modelagem IA utilizando
Lógicas não clássicas
Modal
Temporal
etc...
51/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Métodos especialmente desenvolvidos
Técnicas automáticas de dedução

tableau proof methods

Tradução para lógica clássica
52/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Problema Lógicas não monotonicas
Baseados no método tableau
53/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Métodos para raciocínio automatizado usados com sucesso
em lógicas não clássicas

Extensions of logic programming

Model checking
54/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Extensions of logic programming

Prolog

Abductive logic programing
(Tentativa de imitar raciocínio humano)
55/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Model checking
Utilizado para verificar sistemas concorrentes
É construído um modelo apartir do software expresso
através de uma lógica temporal
Expansão do modelo para sistemas de IA de múltiplos
agentes
56/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Raciocínio sobre ações
 Que ações tomar, dado um determinado estado do
mundo?
 É possível automatizar este tipo de raciocínio a
partir de um formalismo lógico chamado cálculo
situacional (proposto por John McCarthy em 1963)
 Considerar exemplo do elevador.
57/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Cálculo Situacional
• Elementos básicos:
- ações: o que pode ser feito no mundo. Podem ter
pré-condições e efeitos.
* up(n): elevador sobe até andar n.
* open: elevador abre porta.
58/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Cálculo Situacional
• Elementos básicos:
- situações: seqüência de ações, result(a, S) é a
situação que sucede a situação
S após aplicar a ação a
* result(open, result(up(3), S)): elevador subiu até 3o
andar e abriu a porta.
59/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Cálculo Situacional
• Elementos básicos:
- fluents: relações/propriedades cujo valor verdade
pode variar de acordo com a situação.
* on(n, s) indica que o botão está apertado no andar
n na situação s.
* current floor(s) indica qual andar o elevador se
encontra na situação s.
60/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Cálculo Situacional
• Elementos básicos:
- uma pré-condição: Poss(up(n), s)  on(n, s)
61/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Cálculo Situacional
 qual será a situação após “processar” a situação
inicial S0?
current floor(S0) = 2, on(5, S0)
 resposta:
S = result(open, result(up(5), S0))
• quais ações devem ser executadas? basta observar
a situação:
up(5), open
62/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Sistemas Multi-agente
• Como garantir que mensagens trocadas entre
agentes sejam compreendidas/tenham significado?
• Aplicando model checking na comunicação
(compatibilidade com o protocolo).
63/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Raciocínio automático na web
• Utilização de lógica de descrição para representar
ontologias.
- ontologia: descrição de conceitos e relacionamentos
entre conceitos existentes em um domínio do
conhecimento.
• Web-services possuem analogias com sistemas
multi-agente, logo, podem ser utilizadas as mesmas
técnicas para raciocínio.
64/64