taller formas lógica

Taller Conjunto Mexico-Colombia - formas normales, resolucion,
calculo tableaux,- deduccion natural
-Nelson Becerra Correa // Edgar Altamirano Carmona-

1

Conceptos
I Formas Normales
Podemoshablar de dos tipos de formas normales en
l´ gica estas son:
o
a Forma normal conjuntiva en forma abreviada FNCb Forma normal doisyuntiva , en forma abreviada FNDEstas reciben el nombre de acuerdoa sus conectivas, la
disyunci´ n ∨ y conjunci´ n ∧. A continuaci´ n detallao
o
o
mos dichas formas.

• ¬¬Γ ≡ Γ
• ¬(A1 ∨ A2 ) ≡ (¬A1 ∧ ¬A2 )
• ¬(A1 ∧ A2 ) ≡ (¬A1 ∨ ¬A2 )
Repitiendo los pasosanteriores, hasta que la negaci´ n solo afecte a las letras proposicionales
o
c Usar
• A1 ∨ (A2 ∧ A3 ) ≡ (A1 ∨ A2 ) ∧ (A1 ∨ A3 ) ,
para FNC
• A1 ∧ (A2 ∨ A3 ) ≡ (A1 ∧ A2 ) ∨ (A1 ∧ A3 ) ,
para FNDDefinici´ n 1.1 Una formula esta en forma normal con-II An´ lisis de inferencias mediante el m´ todo resoluo
a
e
juntiva, FNC. Si es una o mas conjunci´ n de una o mas cion:
o
disyunciones.Dada una f´ rmula Γ (Un conjunto de f´ rmulas), definio
o
mos la resoluci´ n de la siguiente manera:
o
Ejemplo 1
a A1 es una formula en FNC
a Res0 (Γ) = Γ
b A1 ∧ A2 ∧ A3 es una formula en FNC
bResn+1 (Γ) = Resn (Γ) Res(Resn (Γ))
c (A1 ∨ A2 ∨ A5 ) ∧ (¬A1 ∨ ¬A2 ∨ A5 ) ∧ (¬A7 ∨
c En general, dado un conjunto de cl´ usulas S se
a
A12 ∨ A20 ) es una formula en FNC
tiene:
Definici´ n 1.2 Unaformula esta en forma normal diso
Res(s) = {C:C es resolvente de dos cl´ usulas en S}
a
yuntiva, FND. Si es una mas disyunci´ n de una o mas
o
0
Res (Γ) = Γ
conjunciones.
Res1 (Γ) = Γ Res0(Γ)
Ejemplo 2
a A1 es una formula en FND
Res2 (Γ) = Res1 (Γ) Res0 (Γ)
b A1 ∨ A2 ∨ A3 es una formula en FND
III Tableros semanticos
c (A1 ∧ A2 ∧ A5 ) ∨ (¬A1 ∧ ¬A2 ∧ A5 ) ∨ (¬A7 ∧
IV DeducionNatural
A12 ∧ A20 ) es una formula en FND
El procedimiento de prueba directa en Deduccion NatuEl algoritmo, detalla un m´ todo general para convertir ral es tal como se presenta en el algoritmos :
e...