sl-cap2-8-4-4p

Prévia do material em texto

✬ ✩
2.8.4 TABLEAUX SEMÂNTICOS
Newton José Vieira
UFMG
18 de setembro de 2008
✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Dois tipos de tableaux semânticos
• Baseado no sistema formal SA:
– tableaux com fórmulas marcadas.
• Baseado no sistema formal SB:
– tableaux com fórmulas não marcadas.
Um tableau é a árvore de computação simplificada que resulta da execução de
satA-nd ou satB-nd:
• aquela em que os vértices têm como rótulos A ∪ Σ;
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Tableaux fechados
• Folha fechada: seu rótulo contém literais complementares.
• Folha aberta: seu rótulo não contém literais complementares.
• Tableau fechado: todas as suas folhas são fechadas.
O sistema de tableaux para provar que uma fórmula é tautologia baseia-se em:
α é tautologia se e somente se existe um tableau fechado para Fα (tableau
com fórmulas marcadas) ou para ¬α (tableau com fórmulas não marcadas).
Assim, para verificar se α é tautologia:
verificar se há um tableau fechado para Fα (ou ¬α).
Um algoritmo baseado nessa ideia:
insat (satB-nd determińıstico adaptado para insatisfabilidade).
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Tableaux terminados
Um tableau é dito terminado se cada folha é fechada ou então é aberta mas só
contém literais.
Uma fórmula é insatisfat́ıvel se e somente se um tableau terminado para a mesma é
fechado.
Para determinar se H |= α, basta verificar se H ∪ {¬α} é insatisfat́ıvel:
verificar se um tableau terminado com H ∪ {¬α} na raiz é fechado.
A adaptação de insat para isso é trivial, podendo ser considerado um algoritmo
baseado no sistema SI.
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
Exemplo
A fórmula (p ↔ (¬q ∨ r)) → (¬p → q) é uma tautologia, como mostra o tableau
fechado com fórmulas marcadas:
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
F (p ↔ (¬q ∨ r)) → (¬p → q)
V p ↔ (¬q ∨ r), F¬p → q
V p ↔ (¬q ∨ r), V ¬p, Fq
V p ↔ (¬q ∨ r), Fp, Fq
✏
✏
✏
✏
✏
✏
✏
✏
✏
✏
✏
✏
✏
✏
✏
✏
✏
✏
✏
✏
✏✏
P
P
P
P
P
P
P
P
P
P
P
P
P
P
P
P
P
P
P
P
PP
V p, V ¬q ∨ r, Fp, Fq
X
Fp, F¬q ∨ r, Fq
Fp, F¬q, Fr, Fq
Fp, V q, Fr, Fq
X
c©2007 Newton José Vieira UFMG✫ ✪
✬ ✩
Lógica Aplicada a Computação Cap. 2: Lógica Proposicional
FIM
c©2007 Newton José Vieira UFMG✫ ✪