logica_proposicional

Razonamiento Proposicional en Isabelle

Inteligencia Artificial II - Razonamiento
Proposicional en Isabelle
Omar Monta˜o Rivas
n
Academia de Tecnolog´ de la Informaci´n y Telem´tica,
ıas
o
aUniversidad Polit´cnica de San Luis Potos´
e
ı,
San Luis Potos´
ı

7 de Agosto de 2012

Omar Monta˜o Rivas
n

Introducci´n
o

Razonamiento Proposicional en Isabelle

Consecuentes enIsabelle
Los consecuentes se expresan usando meta-implicaci´n =⇒
o
P1 , P2 , . . . , Pn

Q

es expresado como
P1 =⇒ (P2 =⇒ . . . =⇒ (Pn =⇒ Q) . . .)
o
[|P1 ; P2 ; . . . ; Pn |] =⇒ Q
Lasmeta-implicaciones tambi´n son usadas para expresar
e
relaciones entre las premisas y las conclusiones de las reglas.
P
.
.
.
es escrita como (P =⇒ Q) =⇒ (P → Q)
Q
impI
P→Q
Omar Monta˜o Rivasn

Introducci´n
o

Razonamiento Proposicional en Isabelle

El m´todo rule
e
Usado cuando la conclusi´n de un teorema se unifica con la
o
conclusi´n de estado de prueba actual (o metaactual).
o
Considera el teorema disjI1
P =⇒ P ∨ Q
Si aplicamos rule disjI1 al la meta
[|A; B; C |] =⇒ (A ∧ B) ∨ D
produce la sub-meta
[|A; B; C |] =⇒ (A ∧ B)

Omar Monta˜o Rivas
n

Introducci´no

Razonamiento Proposicional en Isabelle

Matching y Unificaci´n
o
Cuando aplicamos la regla
P =⇒ P ∨ Q
a la meta
[|A; B; C |] =⇒ (A ∧ B) ∨ D
El patr´n P ∨ Q hace match con el objetivo (A∧ B) ∨ D para
o
producir la instanciaci´n P → A ∧ B, Q → D y esto hace al patr´n
o
o
y objetivo iguales.
En general, si la conclusi´n de la meta contiene variables
o
esquem´ticas(meta-variables), las conclusiones se unifican, y las
a
dos son instanciadas para hacerlas iguales.
¡M´s sobre unificaci´n por venir!
a
o

Omar Monta˜o Rivas
n

Introducci´n
o

RazonamientoProposicional en Isabelle

Definici´n general del m´todo rule
o
e
Cuando aplicamos el m´todo rule AlgunaRegla donde
e
AlgunaRegla : [|P1 ; . . . ; Pn |] =⇒ Q
a la meta
[|A1 ; . . . ; Am |] =⇒ C
donde...