Dn Logica Proposicional 2
Inteligencia Artificial II - Deducci´n Natural en o L´gica Proposicional II o
Omar Monta˜o Rivas n
Academia de Tecnolog´ de la Informaci´n y Telem´tica, ıas o a UniversidadPolit´cnica de San Luis Potos´ e ı, San Luis Potos´ ı
7 de Agosto de 2012
Omar Monta˜o Rivas n
Introducci´n o
L´gica Proposicional o
Resumen
L´gica proposicional o
SintaxisSem´ntica a
Deducci´n natural o
reglas de introducci´n y eliminaci´n; o o P Q conjI P ∧Q pruebas (demostraciones) dadas como ´rboles a
La pr´xima clase o
m´s reglas de introducci´n y eliminaci´n a oo las reglas del juego con Isabelle
Omar Monta˜o Rivas n
Introducci´n o
L´gica Proposicional o
Reglas de Eliminaci´n de la Conjunci´n o o
Las reglas de eliminaci´n trabajan endirecci´n opuesta a las o o reglas de introducci´n o P ∧Q P ∧Q conjunct1 conjunct2 P Q Una regla de eliminaci´n de la conjunci´n alternativa es: o o [P] [Q] . . . P ∧Q R conjE R Esta regla puede ser util parapruebas mecanizadas. ´
Omar Monta˜o Rivas n
Introducci´n o
L´gica Proposicional o
Reglas de la Disyunci´n o
Tambi´n hay reglas de introducci´n y eliminaci´n para la e o o disyunci´n: oP disjI 1 P ∨Q [P] . . . R R [Q] . . . R Q disjI 2 P ∨Q
P ∨Q
disjE
Para demostrar R dado P ∨ Q, es suficiente probar R dado P y R dado Q.
Omar Monta˜o Rivas n
Introducci´n o
L´gicaProposicional o
C´lculo de Derivaci´n (Deducci´n Natural) a o o
Notaci´n de consecuente para derivaciones o Γ φ
La conclusi´n φ es derivable de las suposiciones Γ o Las reglas de eliminaci´npueden entonces ser formuladas usando o consecuentes. Por ejemplo, [P] . . . R R [Q] . . . R
P ∨Q
disjE
Puede ser expresado como Γ P ∨Q Γ, P R Γ R Γ, Q R disjE
Introducci´n o
L´gicaProposicional o
Uso de las Reglas de la Disyunci´n o
Probar que B ∨ A es verdadero dado el supuesto que A ∨ B.
Rules: P disjI 1 P ∨Q
A∨B
[A]1 disjI 2 B ∨A B ∨A
[B]1 disjI 1 B ∨ A...
Regístrate para leer el documento completo.