Lógica Proposicional. LEIC - Tagus Park 2 o Semestre, Ano Lectivo 2007/08. c Inês Lynce c Luísa Coheur - PDF
Download "Lógica Proposicional. LEIC - Tagus Park 2 o Semestre, Ano Lectivo 2007/08. c Inês Lynce c Luísa Coheur"
Alícia Costa da Costa
1 Capítulo 2 Lógica Proposicional Lógica para Programação LEIC - Tagus Park 2 o Semestre, Ano Lectivo 2007/08 c Inês Lynce c Luísa Coheur
2 Programa Apresentação Conceitos Básicos Lógica Proposicional ou Cálculo Proposicional Lógica de 1 a ordem ou Lógica de Predicados Programação em Lógica Prolog
3 Programa Apresentação Conceitos Básicos Lógica Proposicional ou Cálculo Proposicional Lógica de 1 a ordem ou Lógica de Predicados Programação em Lógica Prolog
4 Bibliografia Martins J.P., Lógica para Programação, Capítulo 2. Ben-Ari M., Mathematical Logic for Computer Science, Springer-Verlag, 2003, capítulos 2 e 4 (parte) Huth M. e Ryan M., Logic in Computer Science, Cambridge University Press, 2004, capítulos 1 e 6 (parte)
5 Componentes de uma Lógica (relembrar) 1. Linguagem 2. Sistema dedutivo 3. Sistema semântico
6 2 - Sistema dedutivo - o que vamos estudar? Abordagem da dedução natural; Abordagem axiomática; Propriedades do sistema dedutivo; Princípio da resolução.
7 Relembrando, o princípio da resolução é uma regra de inferência derivada α β α γ β γ Res
8 Só que para podermos utilizar o princípio da resolução, as fórmulas têm de estar num formato especial: a forma clausal.
9 Conceitos básicos: literal Um literal é uma fbf atómica (símbolo de proposição) ou a sua negação (no primeiro caso diz-se um literal positivo, no segundo um literal negativo).
10 Exemplo Sendo P e Q símbolos de proposição, as fbfs P e Q são literais, respectivamente positivo e negativo.
11 Conceitos básicos: cláusula Uma cláusula é uma disjunção de literais; Uma cláusula que tem exactamente um literal diz-se uma cláusula unitária.
12 Exemplo Sendo P e Q símbolos de proposição, P Q é uma cláusula.
13 Conceitos básicos: forma clausal Uma fbf na forma clausal corresponde a uma conjunção de cláusulas.
14 Vamos então ver como passar uma fórmula para a forma clausal mas fiquem já a saber que: QUALQUER fbf pode ser transformada numa fbf equivalente na forma clausal.
15 Exercício Tomem nota da seguinte fórmula: (P (Q (R (Q P)))), que vamos usar para ilustrar as diferentes etapas.
16 Conversão para a forma clausal - I Eliminação da equivalência α β (α β) (β α) Eliminação da implicação α β α β (ou α β (α β))
17 Conversão para a forma clausal - II Redução do domínio da negação Aplicação das leis de DeMorgan (α β) α β (α β) α β Eliminação da dupla negação α α
18 Conversão para a forma clausal - III Aplicação da regra da distributividade (da disjunção em relação à conjunção) α (β φ) (α β) (α φ) (α β) φ (α φ) (β φ)
19 Atenção: CNF! Após a etapa anterior a fórmula diz-se na Forma Conjuntiva Normal (ou CNF: conjuctive normal form), isto é, a fórmula é uma conjunção de disjunções.
20 Conversão para a forma clausal - IV Eliminação da conjunção: transformar a fórmula num conjunto de conjuntos de cláusulas; Eliminação da disjunção: transformar cada cláusula num conjunto de literais.
21 Conceitos básicos: cláusula - nova versão Pode-se dizer agora que uma cláusula é um conjunto de literais.
22 Vamos a um exercício?
23 Para que não restem dúvidas: qual a relação entre a forma clausal e a CNF? Qualquer fbf em CNF pode ser transformada numa fbf equivalente na forma clausal.
24 Exemplo A fbf em CNF ( Q P R) (Q P) (Q P R) é equivalente à fbf na forma clausal {{ Q, P, R}, {Q, P}, {Q, P, R}} (ou {QPR, QP, QPR} usando uma notação mais compacta).
25 Voltando ao princípio da resolução, relembrar: α β α γ β γ Res
26 Aplicação da regra de resolução Sejam C 1, C 2 duas cláusulas e α um literal tal que tal que α C 1 e α C 2. Pela aplicação da regra da resolução podemos inferir a cláusula: (C 1 {α}) (C 2 { α})
27 Conceito: resolvente A cláusula resultante da aplicação do princípio da resolução é representada por Res(C 1, C 2 ) = (C 1 {α}) (C 2 { α}) e é denominada resolvente.
28 Vamos lá ver se percebemos o que isto quer dizer com base nos seguintes exemplos 1. ({P, P Q}, Q) 2. ({P Q, Q R}, P R)
29 Demonstração por resolução Corresponde a uma prova no sistema de dedução natural com a diferença as fbf são escritas sob a forma de cláusulas e apenas usamos duas regras de inferência: a regra das premissas e o princípio da resolução.
30 Demonstração por absurdo/por refutação Adicionar a negação da conclusão às premissas e tentar gerar uma contradição, ou seja, a cláusula vazia.
31 Exercício {{ P, Q}, { Q, R}, { R, S}, {P}} {S} (provar por resolução simples e por refutação)
32 Aplicação não controlada da resolução A aplicação não controlada da resolução pode originar muitas inferências inúteis, ou seja, pode levar à: múltipla derivação da mesma cláusula; derivação de cláusulas que não levam ao resultado desejado.
33 Solução: definir estratégias de resolução Geração por saturação de níveis Resolução unitária (não é completa) Resolução linear
34 Geração por saturação de níveis Separar as cláusulas geradas em vários níveis; cada um utiliza pelo menos uma das cláusulas existentes no nível anterior.
35 Resolução unitária (não completa) Cada operação de resolução usa sempre uma cláusula unitária (esta estratégia tem como objectivo reduzir o número de literais existentes nas cláusulas).
36 Exemplo: Resolução unitária {{P, Q}, { P, Q}, {P, Q}, { P, Q}} { Q}
37 O que quer dizer a estratégia de resolução não ser completa? Relembrar: numa lógica completa podem-se demonstrar todos os argumentos válidos.
38 Resolução linear Para gerar cada resolvente, usar sempre uma cláusula inicial e depois um dos sucessores dessa cláusula (denominado cláusula central).
39 Exemplo: Resolução linear {{P, Q}, { P, Q}, {P, Q}, { P, Q}} { Q} (cláusula central {P, Q})
Capítulo 3 Lógica de Primeira Ordem Lógica para Programação LEIC - Tagus Park 1 o Semestre, Ano Lectivo 2007/08 c Inês Lynce and Luísa Coheur Bibliografia Baseados nos slides de Andrew Rice, Universidade
Lógica Computacional DCC/FCUP 2017/18
2017/18 Funcionamento da disciplina Docentes: Teóricas: Sandra Alves Práticas: Sandra Alves e Nelma Moreira Página web http://www.dcc.fc.up.pt/~sandra/home/lc1718.html (slides de aulas e folhas de exercícios,
Lógica Computacional Aula 1
Lógica Computacional Aula 1 DCC/FCUP 2017/18 Funcionamento da disciplina Docentes: Teóricas: Sandra Alves Práticas: Sandra Alves e Nelma Moreira Página web http://www.dcc.fc.up.pt/~sandra/home/lc1718.html
Lógica Computacional Nelma Moreira: T, PL02,PL03 Rogério Reis: PL01,PL04 Departamento de Ciência de Computadores da FCUP Lógica Computacional Aula 1 www.dcc.fc.up.pt/~nam/web/teaching/lc16/index.html Cursos:
Linguagens Lógicas. Aluno: Victor Rocha
Linguagens Lógicas Aluno: Victor Rocha Roteiro Introdução Cálculo de Predicados Proposições Conectores Lógicos Variáveis Tipos de Cláusulas fatos regras Banco de Dados Prolog Fatos em Prolog Questões Unificação
Inteligência Artificial 2016/2017. Grupo 1 Perguntas obrigatórias (15 Minutos)
EI (diurno e PL) ETI (diurno e PL) IGE (diurno e PL) Inteligência Artificial 2016/2017 Teste Tipo de Sistemas Baseados em Conhecimento Lê cuidadosamente as instruções desta prova feita em moldes não habituais.
Inteligência Artificial Taguspark Segundo Teste 14 de Junho de 006 9H00-10H30 Nome: Número: Este teste tem 8 perguntas e 11 páginas. Escreva o número em todas as páginas. Deve ter na mesa apenas o enunciado