Lógica/Cálculo Proposicional Clássico/Dedução Natural - Parte I/Resolução dos Exercícios

De testwiki
Ir para a navegação Ir para a procura

Resolução dos Exercícios de Regras de Inferência Direta

Lembre-se que a ordem na qual as derivações são feitas pode variar.

1

{A↔(B∨C),¬¬B}⊢A∧B

 
1.   A↔(B∨C)   Premissa
2.   ¬¬B   Premissa
3.   B   2 DN
4.   B∨C   3 E
5.   (B∨C)→A   1 BC
6.   A   5,4 MP
7.   A∧B   6,3 C

2

{A∨B,B→C,¬A∧D}⊢C

 
1.   A∨B   Premissa
2.   B→C   Premissa
3.   ¬A∧D   Premissa
4.   ¬A   3 S
5.   B   1,4 SD
6.   C   2,5 MP

3

{A→C,C→A,(A↔C)→B}⊢B

 
1.   A→C   Premissa
2.   C→A   Premissa
3.   (A↔C)→B   Premissa
4.   A↔C   1,2 CB
5.   B   3,4 MP

Resolução dos Exercícios de Regras Hipotéticas

1

P→Q⊢P→(Q∨C)

 
1.   P→Q   Premissa
 
2.     P   Hipótese
3.     Q   1,2 MP
4.     Q∨C   3 E
5.   P→(Q∨C)   2,4 RPC

2

P→¬P⊢¬P

 
1.   P→¬P   Premissa
 
2.     P   Hipótese
3.     ¬P   1,2 MP
4.     P∧¬P   2,3 C
5.   ¬P   2,4 RAA

3

A∨B⊢¬A→B

 
1.   A∨B   Premissa
 
2.     ¬A   Hipótese
3.     B   1,2 SD
4.   ¬A→B   2,3 RPC

4

A→B⊢¬(A∧¬B)

 
1.   A→B   Premissa
 
2.     A∧¬B   Hipótese
3.     A   2 S
4.     ¬B   2 S
5.     B   1,3 MP
6.     B∧¬B   5,4 C
7.   ¬(A∧¬B)   2,6 RAA

5

{¬(A∧B),A}⊢¬B

 
1.   ¬(A∧B)   Premissa
2.   A   Premissa
 
3.     B   Hipótese
4.     A∧B   2,3 C
5.     (A∧B)∧¬(A∧B)   1,4 C
6.   ¬B                           3,5 RAA

Predefinição:AutoCat