Capı́tulo 2
Lógica Proposicional
Lógica para Programação
LEIC - Tagus Park
o
2 Semestre, Ano Lectivo 2007/08
c
Inês
Lynce
c
Luı́sa
Coheur
Programa
• Apresentação
• Conceitos Básicos
• Lógica Proposicional ou Cálculo Proposicional
• Lógica de 1a ordem ou Lógica de Predicados
• Programação em Lógica
• Prolog
Programa
• Apresentação
• Conceitos Básicos
• Lógica Proposicional ou Cálculo Proposicional
• Lógica de 1a ordem ou Lógica de Predicados
• Programação em Lógica
• Prolog
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)
Componentes de uma Lógica (relembrar)
1. Linguagem
2. Sistema dedutivo ← o que estivémos a dar até agora...
3. Sistema semântico
Componentes de uma Lógica (relembrar)
1. Linguagem
2. Sistema dedutivo
3. Sistema semântico ← o que vamos começar a dar hoje...
Sistema Semântico
1. O que acontece num sistema semântico?
2. Conceitos básicos
3. Como obter o valor lógico de uma fbf?
4. Diagramas de decisão binários (BDDs)
5. Diagramas de decisão binários ordenados (OBDDs)
Sistema Semântico
1. O que acontece num sistema semântico?
2. Conceitos básicos
3. Como obter o valor lógico de uma fbf?
4. Diagramas de decisão binários (BDDs)
5. Diagramas de decisão binários ordenados (OBDDs)
O que acontece num sistema semântico?
• Num sistema semântico consideram-se as fbfs e os sı́mbolos
lógicos sob o ponto de vista do seu significado (e não da sua
forma).
O que acontece num sistema semântico?
• Num sistema semântico o valor lógico de uma fbf depende
apenas dos valores lógicos das fbfs que a compõem e dos
sı́mbolos lógicos que relacionam esses componentes.
Sistema Semântico
1. O que acontece num sistema semântico?
2. Conceitos básicos
3. Como obter o valor lógico de uma fbf?
4. Diagramas de decisão binários (BDDs)
5. Diagramas de decisão binários ordenados (OBDDs)
Conceitos básicos – função de valoração
• No sistema semântico da lógica proposicional, uma função de
valoração v é uma função que faz corresponder a cada
sı́mbolo de proposição o valor Verdadeiro (V) ou Falso (F):
– v : P 7→ {V , F }
Conceitos básicos – Satisfação
• Dado um sı́mbolo de proposição P e uma função de valoração
v , diz-se que:
– v satisfaz P se e só se v (P) = V (diz-se também que P é
verdadeiro segundo a função de valoração v );
– v não satisfaz P caso contrário.
Exemplo
• Sejam
– A o sı́mbolo que representa “O IST tem dois campus”;
– B o sı́mbolo que representa “A cadeira de LP é fácil”;
– v uma função de valoração tal que v (A) = T e v (B) = F .
• Nesta situação, v satisfaz A e não satisfaz B.
Conceitos básicos – interpretação
• Dada uma fbf α que contenha os sı́mbolos de proposição P1 ,
..., Pn , uma interpretação é uma função de valoração que
atribui valores a todos esses sı́mbolos de proposição.
Sistema Semântico
1. O que acontece num sistema semântico?
2. Conceitos básicos
3. Como obter o valor lógivo de uma fbf
4. Diagramas de decisão binários (BDDs)
5. Diagramas de decisão binários ordenados (OBDDs)
Então e como é que se obtém o valor lógivo de uma fbf?
Se a fbf for um sı́mbolo de predicado...
• ... esse valor lógico é dado directamente pela função de
valoração.
Se a fbf contiver sı́mbolos lógicos...
• ... há que definir o significado dos sı́mbolos lógicos
(¬, ∧, ∨, →).
• ...
Tabelas de verdade para ¬, ∧, ∨, →
α
V
V
F
F
β
V
F
V
F
α∧β
V
F
F
F
α
V
V
F
F
α
V
F
¬α
F
V
β
V
F
V
F
α∨β
V
V
V
F
α
V
V
F
F
β
V
F
V
F
α→β
V
F
V
V
... e depois de definir o significado dos sı́mbolos lógicos...
• ... os valores lógicos da fbf são obtidos através da composição
dos valores lógicos das suas fbfs.
Exemplo: (A ∧ B) → (¬A ∨ ¬B)
A
V
V
F
F
B
V
F
V
F
A∧B
V
F
F
F
¬A ∨ ¬B
F
V
V
V
(A ∧ B) → (¬A ∨ ¬B)
F
V
V
V
Só que há um problema com este método...
• ... a dimensão da tabela de verdade cresce exponencialmente
em função do número de predicados.
Mas antes de avançar para uma solução...
• ... vamos fixar um conjunto de conceitos.
Conceitos: fbfs tautológicas, satisfazı́veis, falsificáveis e
contraditórias
• Tautológicas: verdadeiras para todas as interpretações
• Satisfazı́veis: existe pelo menos uma interpretação na qual a
fbf é verdadeira
• Falsificável: existe pelo menos uma interpretação na qual a fbf
é falsa
• Contraditórias (ou não satisfazı́veis): falsas para todas as
interpretações
Exemplos
• (P ∨ Q) é satisfazı́vel e falsificável;
• P ∨ ¬P é tautológica;
• (P ∧ ¬P) é contraditória.
Conceitos: conjunto satisfazı́vel/contraditório e modelo
• Um conjunto de fbfs diz-se satisfazı́vel sse existe pelo menos
uma interpretação (dita um modelo) que satisfaz todas as
suas fórmulas;
• Um conjunto de fbfs diz-se contraditório sse não existe
nenhuma interpretação que satisfaz todas as suas fórmulas.
Exemplos
• O conjunto {P, Q, P → Q}, pois a interpretação v (P) = V e
v (Q) = V satisfaz todas as suas fórmulas (e é portanto um
modelo desse conjunto);
• O conjunto {P, ¬P} é contraditório, pois não existe nenhuma
interpretação que satisfaça todas as suas fórmulas.
Sistema Semântico
1. O que acontece num sistema semântico?
2. Conceitos básicos
3. Como obter o valor lógico de uma fbf
4. Diagramas de decisão binários (BDDs)
5. Diagramas de decisão binários ordenados (OBDDs)
Diagramas de decisão binários (Binary Decision Diagrams
– OBDDs)
• Para se conseguir determinar de um modo mais eficiente o
valor lógico das fbfs vamos estudar os BDDS.
Diagramas de decisão binários (Binary Decision Diagrams
– OBDDs)
• Mas antes de chagar aos BDDs, há que apresentar um
conjunto de conceitos...
Conceito – Árvores de decisão binárias
• Nós
–
–
• Nós
–
não terminais:
são rotulados com os sı́mbolos de predicado da fbf;
cada um tem dois arcos: um tracejado e outro cheio;
terminais:
são rotulados com 0/1 (Falso/Verdadeiro).
Exemplo: Árvore binária para ¬(x ∨ y )
x
y
1
y
0
0
0
Árvore de decisão binária finita (cont)
• Uma árvore de decisão binária finita determina uma única
função Booleana definida em função dos sı́mbolos de
predicado que constam nos nós não terminais.
• Dada uma interpretação para os sı́mbolos proposicionais,
começamos pela raı́z da árvore e seguimos o arco no sentido
descendente tracejado/cheio no caso da interpretação do
sı́mbolo proposicional ser F/V
Exemplo: Árvore binária para ¬(x ∨ y )
x
y
1
y
0 0
0
• valor lógico para a interpretação x = F , y = V
x
y
1
y
0
0
0
E qual a relação com as tabelas de verdade?
Exemplo: tabela de verdade para ¬(x ∨ y )
x
V
V
F
F
¬(x ∨ y )
F
F
F
V
y
V
F
V
F
x
y
1
y
0
0
0
E qual a vantagem em relação às tabelas de verdade?
• Árvores de decisão binária têm uma dimensão semelhante às
tabelas de verdade
– MAS as árvores de decisão binária contêm redundâncias que
podem ser eliminadas!
Definição formal de BDDs
• Antes de definir formalmente o que é um BDD, vamos ter de
introduzir as definições de grafo dirigido e grafo dirigido
acı́clico
Conceito: grafo dirigido
• Um grafo dirigido é um par (N , A) em que:
– N é um conjunto de elementos chamados nós;
– A é um conjunto de arcos.
Conceito: arco
• Um arco é um par ordenado cujos elementos são nós, sendo
cada arco (ni , nj ) caracterizado pelo nó de partida ni e pelo
nó de chegada nj .
Conceito: ciclo
• Um ciclo num grafo dirigido é um caminho finito num grafo
que começa e termina num mesmo nó.
Exemplo: ciclo
• Um caminho com a forma n1 → n2 → . . . → nm → n1 é um
ciclo.
Conceito: grafo dirigido acı́clico (DAG)
• Um grafo dirigido acı́clico (DAG, do Inglês Directed Acyclic
Graph) é um grafo dirigido que não contém ciclos.
Conceito: nós iniciais/finais num DAG)
• Um nó num DAG é um nó inicial se não existem arcos que
terminem nesse nó;
• Um nó num DAG é um nó final se não existem arcos que
tenham inı́cio nesse nó.
Exemplo: grafo dirigido acı́clico
Conceito: definição formal de BDD
• Um
–
–
–
BDD é um DAG finito com as seguintes caracterı́sticas:
Tem um único nó inicial
Todos os nós terminais são rotulados com 1/0
Todos os nós não terminais são rotulados com um sı́mbolo
proposicional
– Cada nó não terminal é o nó inicial para dois arcos, em que
um arco é representado a tracejado e outro arco é representado
a cheio (correspondentes aos rótulos 0/1, respectivamente)
– Nota: considera-se que os arcos têm o sentido descendente
Exemplo: BDDs B0 e Bx
x
0
0
1
A seguir vamos ver...
• ... como é que os as redundâncias das BDDs podem ser
eliminadas através de um conjunto de passos chamados
reduções (porque permitem reduzir o tamanho do BDD).
Reduções em BDDs
• R1: Remoção de folhas duplicadas
• R2: Remoção de testes redundantes
• R3: Remoção de nós redundantes
• Nota: um BDD diz-se reduzido se nenhuma destas reduções
puder ser aplicada
R1: Remoção de folhas duplicadas
• Se um BDD contém mais do que um nó terminal com os
rótulos 0/1, então podemos redireccionar todos os arcos
dirigidos para nós com o rótulo 0/1 para apenas um nó.
• Nota: na prática existe no máximo um nó com o rótulo V e
um nó com o rótulo F.
Exemplo: Remoção de folhas duplicadas
x
x
y
1
y
y
0
0
0
1
y
0
R2: Remoção de testes redundantes
• Se os dois arcos que saem de um nó n se dirigem a um mesmo
nó m então podemos eliminar o nó n e direccionar os arcos
para o nó m
• Por cada nó eliminado, é eliminado um par de arcos
tracejados/cheios
Exemplo: remoção de testes redundantes
x
x
y
1
y
0
y
1
0
R3: Remoção de nós redundantes
• Se dois nós distintos n e m são raı́z de dois sub-BDDs
estruturalmente equivalentes, então podemos eliminar o nó m
e dirigir todos os arcos para o nó n.
• Nota: a remoção de folhas duplicadas é um caso especial da
remoção de nós redundantes.
Exemplo: BDD com sub-BDDs duplicadas
z
x
x
y
y
0
y
y
1
Exemplo: remoção de nós redundantes
z
z
x
x
x
y
y
y
0
1
y
y
0
1
Vamos lá fazer uns exercı́cios!
Mas então...
• tudo bem que conseguimos reduzir os BDDs...
• ... mas antes de chegar ao BDD reduzido temos de construir
previamente a árvore de decisão binária, mantendo-se o
problema de complexidade exponencial que já tı́nhamos com
as tabelas de verdade...
E então que ganhamos com isto tudo?
É que podemos fazer composição de BDDs!
• Ou seja, podemos construir um BDD para uma fbf a partir de
BDDs (já reduzidas) que correspondem a componentes da fbf.
E como é que é feita essa composição?
• BDD para ¬α construı́da a partir do BDD para α (BDDα ):
nós terminais com rótulo 0/1 substituı́dos por nós terminais
com rótulo 1/0
• BDD para α ∧ β construı́da a partir do BDDα : nó com rótulo
1 substituı́do pela BDDβ ; de seguida aplicar transformações
• BDD para α ∨ β construı́da a partir do BDDα : nó com rótulo
0 substituı́do pela BDDβ ; de seguida aplicar transformações
Exemplo: BDDs B e ¬B
x
x
y
1
y
y
0 0
0
0
y
1
1
1
Vamos lá ver outros exemplos
Só que a composição pode não correr sempre bem com
BDDs
Basicamente porque...
• ... nada impede que um mesmo sı́mbolo proposicional apareça
num caminho de um BDD mais do que uma vez.
Exemplo: sı́mbolo repetido
x
y
x
z
y
0
x
1
Aliás...
• O mesmo sı́mbolo pode aparecer mais do que uma vez (por
exemplo quando um BDD é construı́da usando composição).
E o problema é que...
• ... BDDs com múltiplas ocorrências de um mesmo sı́mbolo
proposicional ao longo de um caminho não são eficientes, pois,
por exemplo, passa a ser difı́cil detectar BDDs equivalentes;
Exemplo: BDDs equivalentes
x
x
y
z
y
x
y
y
x
z
0
1
0
1
Então há que arranjar uma alternativa...
• ... uma solução passa por impôr uma ordem aos sı́mbolos
proposicionais!
E surge então o conceito de BDDs ordenados, isto é,
OBDDs