Verificação Formal de Software

1.4. Equivalência Lógica🔗

Uma valoração atribui um valor de verdade a cada variável proposicional. Uma proposição é uma tautologia quando é verdadeira sob toda valoração. Duas proposições A e B são logicamente equivalentes, escrito A ≡ B, quando têm o mesmo valor de verdade sob toda valoração, isto é, quando A ↔ B é uma tautologia.

As equivalências clássicas abaixo aparecem constantemente em provas.

Nome

Equivalência

De Morgan

¬(P ∧ Q) ≡ ¬P ∨ ¬Q

De Morgan

¬(P ∨ Q) ≡ ¬P ∧ ¬Q

Dupla negação

¬¬P ≡ P

Contrapositiva

P → Q ≡ ¬Q → ¬P

Implicação material

P → Q ≡ ¬P ∨ Q

Uma tabela-verdade verifica cada equivalência. Para a segunda lei de De Morgan, as colunas de ¬(P ∨ Q) e de ¬P ∧ ¬Q coincidem nas quatro valorações.

P

Q

P ∨ Q

¬(P ∨ Q)

¬P

¬Q

¬P ∧ ¬Q

V

V

V

F

F

F

F

V

F

V

F

F

V

F

F

V

V

F

V

F

F

F

F

F

V

V

V

V

Tabelas-verdade decidem qualquer questão proposicional, mas o seu tamanho cresce exponencialmente no número de variáveis, e elas não se estendem aos quantificadores da Aula 2. Regras de dedução, aplicadas um passo por vez, escalam e generalizam. O restante desta aula desenvolve tais provas em Lean.