Prototipo de Smart Home automatizado con IoT IoT automated ...
1/64 Resumo do Artigo Automated Reasoning Felipe S. Boffo Fernando dos Santos Leomar Costa Leonardo...
Transcript of 1/64 Resumo do Artigo Automated Reasoning Felipe S. Boffo Fernando dos Santos Leomar Costa Leonardo...
1/64
Resumo do Artigo “Automated Reasoning”
Felipe S. Boffo
Fernando dos Santos
Leomar Costa
Leonardo Couto
Roger Reis
2/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 )
3/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
é uma conseqüência lógica do conjunto S de suposições ?
4/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
5/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
6/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
7/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.
8/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 por um taco.
9/64
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.
10/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.
11/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.
12/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
13/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Teorema indutivo de prova não é nem mesmo semi-decidí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
14/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;
15/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
16/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
17/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Lógicas de maior ordem (, )
Até mesmo teorema dedutivo de prova não são semi-decidí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.
18/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 ...
19/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.
20/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.
21/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
22/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.
23/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 ...
24/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.
25/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.
26/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.
27/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.
28/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.
29/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.
30/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.
31/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Decidível prático
Problemas de raciocínio decidível são tipicamente NP-completos
Raciocínio automático confia no paradigma de pesquisa da inteligência artificial.
32/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.
33/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.
34/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.
35/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.
36/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.
37/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.
38/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Estratégias
Raciocínio postergadoEstas 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
39/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.
40/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Estratégias
Redução a subobjetivosTratam 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.
41/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.
42/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.
43/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.
44/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
45/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
46/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Aplicações
Provadores de teoremas foram aplicados com sucesso emVerificação de protocolos criptográficosSistemas orientados a mensagensEspecificações de software
47/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
48/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
49/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
50/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.
.
51/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Modelagem IA utilizando
Lógicas não clássicas
Modal
Temporal
etc...
52/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
53/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Problema Lógicas não monotonicas
Baseados no método tableau
54/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
55/64
Lógica Aplicada – Resumo do Artigo “Automated Reasoning”
Extensions of logic programming
Prolog
Abductive logic programing(Tentativa de imitar raciocínio humano)
56/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
57/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.
58/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.
59/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.
60/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.
61/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)
62/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
63/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).
64/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.