Inteligencia Artificial Oscar Bedoya
[email protected] http://eisc.univalle.edu.co/~oscarbed/IA/
* Inferencia en lógica de predicados * Forma canónica * Forma normal conjuntiva
Lógica y Agentes Agentes basados en conocimiento 1 1
2 3 4
5
2
3
4
5
6
Lógica y Agentes Agentes basados en conocimiento - Lógica proposicional - Lógica de predicados
BC
- Prolog
Lógica y Agentes Agentes basados en conocimiento maullido(1,1) maullido(1,2) maullido(1,3) maullido(1,4) maullido(1,5) maullido(1,6) maullido(3,1)
gato(1,2) gato(1,1) gato(1,2) gato(1,3) gato(1,4) gato(1,5) gato(2,1)
maullido(1,1)gato(1,2) maullido(1,2)gato(1,1) maullido(1,3)gato(1,2) maullido(1,4)gato(1,3) maullido(1,5)gato(1,4) maullido(1,6)gato(1,5)
gato(2,1) gato(2,2) gato(2,3) gato(2,4) gato(2,5) gato(2,6) gato(3,2)
gato(2,1) gato(2,2) gato(2,3) gato(2,4) gato(2,5) gato(2,6)
1 1
gato(1,3) gato(1,4) gato(1,5) gato(1,6) gato(4,1)
gato(1,3) gato(1,4) gato(1,5) gato(1,6)
2 3 4 5
2
3
4
5
6
Lógica y Agentes Agentes basados en conocimiento maullido(1,1) maullido(1,2) maullido(1,3) maullido(1,4) maullido(1,5) maullido(1,6) maullido(3,1)
gato(1,2) gato(1,1) gato(1,2) gato(1,3) gato(1,4) gato(1,5) gato(2,1)
gato(2,1) gato(2,2) gato(2,3) gato(2,4) gato(2,5) gato(2,6) gato(3,2)
1 1
gato(1,3) gato(1,4) gato(1,5) gato(1,6) gato(4,1)
2 3 4 5
2
3
4
5
6
Lógica y Agentes Agentes basados en conocimiento 1
2
3
4
5
6
1 2 3 4 5
i j
maullido(i,j) gato(i,j-1)
gato(i,j+1)
gato(i+1,j)
gato(i-1,j)
Lógica y Agentes Dada la siguiente base de conocimientos convierta a notación de conjuntos y demuestre c 1. b d 2. da 3. a( b c)
La base de conocimientos está en lógica proposicional (no hay cuantificadores)
Modus Ponens
Resolución unitaria
________
________
Y-Eliminación ... ________
1
2
n
i
Y-Introducción ... n ________ 1 2 . . . n 1
2
O-Introducción 1
________ 1
Las reglas de inferencia se definieron para sentencias en lógica proposicional
Lógica y Agentes
1.
x P(x)Q(x)
2. x R(x) 3.
x Q(x) R(x)
¿Cómo inferir cuando se tienen sentencias cuantificadas (lógica de predicados)?
Inferencia en lógica de predicados Represente las sentencias dadas en el siguiente enunciado: Todos los hombres son mortales Sócrates es un hombre
Demostrar “Sócrates es mortal”
Inferencia en lógica de predicados Represente las sentencias dadas en el siguiente enunciado: Todos los hombres son mortales Sócrates es un hombre
1.
x Hombre(x) Mortal(x)
2. Hombre(Sócrates)
Inferencia en lógica de predicados Términos base
• Los términos base no contienen variables lógicas • Solo pueden ser una constante o un predicado aplicado sobre valores 1.
x Hombre(x) Mortal(x)
1.
x juega(Cali,x) gana(x)
2. Hombre(Sócrates) Término base Término base
Inferencia en lógica de predicados Dos nuevas reglas de inferencia
• Eliminación universal • Eliminación existencial
Modus Ponens
Resolución unitaria
________
________
Y-Eliminación ... ________
1
2
n
i
Y-Introducción ... n ________ 1 2 . . . n 1
2
O-Introducción 1
________ 1
Modus Ponens
Resolución unitaria
________
________
Y-Eliminación 1 2 . . . ________
n
Eliminación universal
i
Y-Introducción ... n ________ 1 2 . . . n 1
2
O-Introducción 1
________ 1
Eliminación existencial
Inferencia en lógica de predicados Dos nuevas reglas de inferencia
• Eliminación universal x ________
SUST({x/g}, )
donde x es una variable y g es un término base
Inferencia en lógica de predicados Dos nuevas reglas de inferencia
• Eliminación universal x ________
SUST({x/g}, )
BC:
1. x LeGusta(x, ElHelado)
Inferencia en lógica de predicados Dos nuevas reglas de inferencia
• Eliminación universal x ________
SUST({x/g}, )
BC:
1. x LeGusta(x, ElHelado) 2. LeGusta(Ben,ElHelado)
Elim-Universal(1),
={x/Ben}
Inferencia en lógica de predicados Dos nuevas reglas de inferencia
• Eliminación universal x ________
SUST({x/g}, )
BC:
1. x LeGusta(x, ElHelado) 2. LeGusta(Ben,ElHelado)
Elim-Universal(1),
={x/Ben}
3. LeGusta(Juan,ElHelado)
Elim-Universal(1),
={x/Juan}
Inferencia en lógica de predicados Dos nuevas reglas de inferencia
• Eliminación existencial x ________
SUST({x/k}, )
donde x es una variable y k es un símbolo de constante que no aparece en la base de conocimientos inicial
Inferencia en lógica de predicados Dos nuevas reglas de inferencia
• Eliminación existencial x ________
SUST({x/k}, )
BC: 1. x Matar(x,Juan) 2. Amigo(Luis,Juan)
Inferencia en lógica de predicados Dos nuevas reglas de inferencia
• Eliminación existencial x ________
SUST({x/k}, )
BC: 1. x Matar(x,Juan) 2. Amigo(Luis,Juan)
3. Matar(Pedro,Juan)
Elim-Existencial (1), ={x/Pedro}
Inferencia en lógica de predicados Dos nuevas reglas de inferencia
• Eliminación existencial x ________
SUST({x/k}, )
BC:
No se puede realizar la sustitución {x/Luis}
1. x Matar(x,Juan) 2. Amigo(Luis,Juan)
3. Matar(Pedro,Juan)
Elim-Existencial (1), ={x/Pedro}
Modus Ponens
Resolución unitaria
________
________
Y-Eliminación ... ________
1
2
n
i
Y-Introducción ... n ________ 1 2 . . . n 1
2
O-Introducción 1
________ 1
Modus Ponens
Resolución unitaria
________
________
Y-Eliminación
Eliminación universal
... ________
1
2
n
i
Y-Introducción ... n ________ 1 2 . . . n 1
2
O-Introducción 1
________ 1
x ________ SUST({x/g}, ) Eliminación existencial x ________ SUST({x/k}, )
Inferencia en lógica de predicados Represente las sentencias dadas en el siguiente enunciado: Todos los hombres son mortales Sócrates es un hombre
Pruebe que “Sócrates es mortal”
Inferencia en lógica de predicados Represente las sentencias dadas en el siguiente enunciado: Todos los hombres son mortales Sócrates es un hombre
Pruebe que “Sócrates es mortal”
1.
x Hombre(x) Mortal(x)
2. Hombre(Sócrates) Demostrar Mortal(Sócrates)
Inferencia en lógica de predicados
1.
x Hombre(x) Mortal(x)
2. Hombre(Sócrates)
Inferencia en lógica de predicados
1.
x Hombre(x) Mortal(x)
2. Hombre(Sócrates) 3. Hombre(?) Mortal(?), Elim-Universal (1), ={x/?}
Inferencia en lógica de predicados
1.
x Hombre(x) Mortal(x)
2. Hombre(Sócrates) 3. Hombre(DonOmar) Mortal(DonOmar), Elim-Universal (1), ={x/DonOmar}
Inferencia en lógica de predicados
1.
x Hombre(x) Mortal(x)
2. Hombre(Sócrates) 3. Hombre(DonOmar) Mortal(DonOmar), Elim-Universal (1), ={x/DonOmar} 4. Hombre(Socrates) Mortal(Socrates), Elim-Universal (1), ={x/Socrates}
Inferencia en lógica de predicados
1.
x Hombre(x) Mortal(x)
2. Hombre(Sócrates) 3. Hombre(DonOmar) Mortal(DonOmar), Elim-Universal (1), ={x/DonOmar} 4. Hombre(Socrates) Mortal(Socrates), Elim-Universal (1), ={x/Socrates} 5. Mortal(Sócrates), MP(2,4)
Modus Ponens
Resolución unitaria
________
________
Y-Eliminación
Eliminación universal
... ________
1
2
n
i
Y-Introducción ... n ________ 1 2 . . . n 1
2
O-Introducción 1
________ 1
x ________ SUST({x/g}, ) Eliminación existencial x ________ SUST({x/k}, ) Introducción existencial ________ x SUST({g/x}, )
Inferencia en lógica de predicados
1.
x Hombre(x)Mortal(x)
2. Hombre(Sócrates)
Inferencia en lógica de predicados
1.
x
Hombre(x) Mortal(x)
2. Hombre(Sócrates)
Inferencia en lógica de predicados
1.
x
Hombre(x) Mortal(x)
2. Hombre(Sócrates) 3.
Hombre(Sócrates) Mortal(Sócrates), Elim-Universal (1) ={x/Sócrates}
4. Mortal(Sócrates), res(2,3)
1.
w
P(w) Q(w)
2.
x P(x) R(x)
3.
y
Q(y) S(y)
4.
z
R(z) S(z)
Demostrar S(a)
1.
w
P(w) Q(w)
2.
x P(x) R(x)
3.
y
Q(y) S(y)
4.
z
R(z) S(z)
5.
P(a) Q(a), Elim-Universal(1)
6. P(a) R(a), Elim-Universal(2)
={w/a} ={x/a}
7.
Q(a) S(a), Elim-Universal(3)
={y/a}
8.
R(a) S(a), Elim-Universal(4)
={z/a}
9.
P(a) S(a), res(5,7)
10. R(a) S(a), res(6,9) 11. S(a), res(8,10)
1.
w
R(w) P(w) Q(w) S(w)
2.
x
Q(x)
3.
y
S(y) P(y)
4.
z
P(z)
R(x)
R(z)
Demostrar R(a)
1.
w
R(w) P(w) Q(w) S(w)
2.
x
Q(x)
3.
y
S(y) P(y)
4.
z
P(z)
5.
R(a) P(a) Q(a) S(a), Elim-Universal(1)
6.
Q(a)
7.
S(a) P(a), Elim-Universal(3)
8.
P(a)
9.
R(a) P(a) S(a), res(5,6)
10. P(a) 11.
R(x)
R(z) R(a), Elim-Universal(2)
R(a), Elim-Universal(4)
R(a), res(7,9)
R(a), res(8,10)
={x/a}
={y/a} ={z/a}
={w/a}
1. x
P(x)
2.
x P(x) Q(x)
3.
x
Q(x) R(x)
4.
x
S(x) T(x)
5. S(a)
Demostrar R(b) T(a)
1. x
P(x)
2.
x P(x) Q(x)
3.
x
Q(x) R(x)
4.
x
S(x) T(x)
5. S(a) 6.
P(b), Elim-Existencial(1) ={x/b}
x se puede reemplazar por b porque no está en BC inicial
1. x
P(x)
2.
x P(x) Q(x)
3.
x
Q(x) R(x)
4.
x
S(x) T(x)
5. S(a) 6.
P(b), Elim-Existencial(1) ={x/b}
7. P(b) Q(b), Elim-Universal(2) ={x/b} 8.
Q(b) R(b), Elim-Universal(3) ={x/b}
9.
S(a) T(a), Elim-Universal(4) ={x/a}
10. Q(b), res(6,7) 11. R(b), res(8,10) 12. T(a), res(5,9) 13. R(b) T(a), Y-Intro(11,12)
1.
x
2. x
T(x) Q(x) Q(x)
3. P(b) P(c)
4.
x R(x) T(x)
5.
x
P(x)
S(x)
Demostrar R(a)
S(c)
1.
x
2. x
T(x) Q(x) Q(x)
3. P(b) P(c)
4.
x R(x) T(x)
5.
x
P(x)
S(x)
6. P(c), Y-Elim(3)
7.
T(a) Q(a), Elim-Universal(1) ={x/a}
8.
Q(a), Elim-Existencial(2) ={x/a}
9.
T(a), res(7,8)
10. R(a) T(a), Elim-Universal(4) ={x/a}
11. R(a), res(9,10) 12.
P(c)
13.
S(c), res(6,12)
14. R(a)
S(c), Elim-Universal(5) ={x/c}
S(c), Y-Intro(11,13)
1.
x P(x) Q(x)
2.
x
Q(x)
S(x)
3. x S(x)
4. T(c)
Demostrar P(a) P(b)
1. x P(x) Q(x) 2. x
Q(x)
S(x)
3. x S(x) 4. T(c) 5. P(a) Q(a), Elim-Universal(1) ={x/a}
6. Q(a)
S(a), Elim-Universal(2) ={x/a}
7. S(a), Elim-Existencial(3) ={x/a} 8. Q(a), res(6,7)
9. P(a), res(5,8) 10. P(b) Q(b), Elim-Universal(1) ={x/b} 11. Q(b)
S(b), Elim-Universal(2) ={x/b}
12. S(b), Elim-Existencial(3) ={x/b} 13. Q(b), res(11,12)
14. P(b), res(10,13) 15. P(a) P(b), Y-Intro(9,14)
Inferencia en lógica de predicados Modus ponens generalizado
• Logra en un solo paso lo que se requería al aplicar Y-Introducción, Eliminación universal y Modus ponens
Inferencia en lógica de predicados Modus ponens generalizado
• Logra en un solo paso lo que se requería al aplicar Y-Introducción, Eliminación universal y Modus ponens 1. P(a)
2. Q(a) 3.
x (P(x) Q(x))R(x)
Demostrar R(a)
Inferencia en lógica de predicados Modus ponens generalizado
• Logra en un solo paso lo que se requería al aplicar Y-Introducción, Eliminación universal y Modus ponens 1. P(a)
2. Q(a) 3.
x (P(x) Q(x))R(x)
4. (P(a) Q(a))R(a), Elim-Universal (3) ={x/a}
Inferencia en lógica de predicados Modus ponens generalizado
• Logra en un solo paso lo que se requería al aplicar Y-Introducción, Eliminación universal y Modus ponens 1. P(a)
2. Q(a) 3.
x (P(x) Q(x))R(x)
4. (P(a) Q(a))R(a), Elim-Universal (3) ={x/a} 5. P(a) Q(a), Y-Intro(1,2)
Inferencia en lógica de predicados Modus ponens generalizado
• Logra en un solo paso lo que se requería al aplicar Y-Introducción, Eliminación universal y Modus ponens 1. P(a)
2. Q(a) 3.
x (P(x) Q(x))R(x)
4. (P(a) Q(a))R(a), Elim-Universal (3) ={x/a} 5. P(a) Q(a), Y-Intro(1,2) 6. R(a), MP(4,5)
Inferencia en lógica de predicados 1. T(a)
2. S(a) 3.
x (T(x) S(x))P(x)
4. U(a) 5.
x (P(x) U(x))Q(x)
Demostrar Q(a)
Inferencia en lógica de predicados 1. T(a) 2. S(a) 3.
x (T(x) S(x))P(x)
4. U(a)
5.
x (P(x) U(x))Q(x)
6. (T(a) S(a))P(a), Elim-Universal (3) ={x/a} 7. T(a) S(a), Y-Intro(1,2)
8. P(a), MP(6,7) 9. (P(a) U(a))Q(a), Elim-Universal (5) ={x/a} 10. P(a) U(a), Y-Intro(4,8)
11. Q(a), MP(9,10)
Inferencia en lógica de predicados 1. T(a) 2. S(a) 3.
x (T(x) S(x))P(x)
4. U(a)
5.
x (P(x) U(x))Q(x)
6. (T(a) S(a))P(a), Elim-Universal (3) ={x/a} 7. T(a) S(a), Y-Intro(1,2)
8. P(a), MP(6,7) 9. (P(a) U(a))Q(a), Elim-Universal (5) ={x/a} 10. P(a) U(a), Y-Intro(4,8)
11. Q(a), MP(9,10)
• Elim-Univ • Y-Intro • MP • Elim-Univ • Y-Intro • MP
Inferencia en lógica de predicados Modus ponens generalizado p1’ p2’ . . . pn’ (p1 p2 . . . pn q) ____________________________ SUST( ,q)
donde pi’ son términos base y pi son sentencias cuantificadas en las que existe una sustitución pi’=SUST( ,pi) para toda i
tal que
Inferencia en lógica de predicados Modus ponens generalizado p1’ p2’ . . . pn’ (p1 p2 . . . pn q) ____________________________ SUST( ,q)
1. P(a)
2. Q(a) 3.
x (P(x) Q(x))R(x)
Inferencia en lógica de predicados Modus ponens generalizado p1’ p2’ . . . pn’ (p1 p2 . . . pn q) ____________________________ SUST( ,q)
1. P(a)
2. Q(a) 3.
x (P(x) Q(x))R(x)
4. R(a), MPG(1,2,3)
={x/a}
Inferencia en lógica de predicados 1. T(a)
2. S(a) 3.
x (T(x) S(x))P(x)
4. U(a) 5.
x (P(x) U(x))Q(x)
Demostrar Q(a) usando MPG
Inferencia en lógica de predicados 1. T(a)
2. S(a) 3.
x (T(x) S(x))P(x)
4. U(a) 5.
x (P(x) U(x))Q(x)
6. P(a), MPG(1,2,3), ={x/a}
Inferencia en lógica de predicados 1. T(a)
2. S(a) 3.
x (T(x) S(x))P(x)
4. U(a) 5.
x (P(x) U(x))Q(x)
6. P(a), MPG(1,2,3), ={x/a}
7. Q(a), MPG(4,5,6), ={x/a}
Inferencia en lógica de predicados • Si se quisiera aplicar modus ponens generalizado, las sentencias en BC tendrían que ser: - Una implicación con una conjunción en el lado izquierdo y un solo átomo a la derecha - Un término base
Inferencia en lógica de predicados • Si se quisiera aplicar modus ponens generalizado, las sentencias en BC tendrían que ser: - Una implicación con una conjunción en el lado izquierdo y un solo átomo a la derecha. (sentencias Horn) - Un término base
Alfred Horn (1918 - 2001)
Inferencia en lógica de predicados Forma canónica
Cuando la base de conocimientos se forma exclusivamente de sentencias Horn se dice que está en forma canónica
Inferencia en lógica de predicados Cómo convertir una BC a forma canónica
• Se eliminan los cuantificadores existenciales • No es necesario escribir los cuantificadores universales
1. x P(x) 2. x (Q(x) R(x))S(x) 3. T(b) …
1. P(a) 2. (Q(x) R(x))S(x) 3. T(b) …
Inferencia en lógica de predicados 1. T(a)
2. S(a) 3.
x (T(x) S(x))P(x)
4. U(a) 5.
x (P(x) U(x))Q(x)
Convertir a forma canónica
Inferencia en lógica de predicados 1. T(a)
2. S(a) 3. (T(x) S(x))P(x) 4. U(a) 5. (P(x) U(x))Q(x)
1.
x E(x) U(x) M(x) F(x)
2.
x A(x)U(x)
3.
x E(x)M(x)
4. E(a) A(a)
Expresar en forma canónica
1. E(x) U(x) M(x) F(x) 2. A(x)U(x) 3. E(x)M(x)
4. E(a) A(a)
1. E(x) U(x) M(x) F(x) 2. A(x)U(x) 3. E(x)M(x)
4. E(a) A(a)
Demostrar F(a) usando MPG
1. E(x) U(x) M(x) F(x) 2. A(x)U(x) 3. E(x)M(x)
4. E(a) A(a) 5. E(a), Y-Elim(4) 6. A(a), Y-Elim(4)
7. U(a), MPG(2,6) ={x/a} 8. M(a), MPG(3,5) ={x/a} 9. F(a), MPG(1,5,7,8) ={x/a}
1.
x y T(x) R(x,y) P(y) I(x)
2.
x y T(x) J(x) P(y)R(x,y)
3. x P(x)
4. T(a) J(a)
Expresar en forma canónica y demostrar I(a)
1. T(x) R(x,y) P(y) I(x) 2. T(x) J(x) P(y)R(x,y) 3. P(b)
4. T(a) J(a)
1. T(x) R(x,y) P(y) I(x) 2. T(x) J(x) P(y)R(x,y) 3. P(b)
4. T(a) J(a)
Demostrar I(a)
1. T(x) R(x,y) P(y) I(x) 2. T(x) J(x) P(y)R(x,y) 3. P(b)
4. T(a) J(a) 5. R(a,b), MPG(2,3,4) ={x/a, y/b} 6. T(a), Y-Elim(4)
7. I(a), MPG(1,3,5,6), ={x/a, y/b}
1.
x R(x) J(x) C(x)S(x,a)
2.
x C(x) R(x)E(x,b)
3.
x E(x,b) R(x) S(x,a)S(x,c)
4. R(u) J(u) C(u)
Expresar en forma canónica y demostrar S(u,c)
1. R(x) J(x) C(x)S(x,a) 2. C(x) R(x)E(x,b) 3. E(x,b) R(x) S(x,a)S(x,c)
4. R(u) J(u) C(u)
1. R(x) J(x) C(x)S(x,a) 2. C(x) R(x)E(x,b) 3. E(x,b) R(x) S(x,a)S(x,c)
4. R(u) J(u) C(u)
Demostrar S(u,c)
1. R(x) J(x) C(x)S(x,a)
2. C(x) R(x)E(x,b) 3. E(x,b) R(x) S(x,a)S(x,c) 4. R(u) J(u) C(u)
5. R(u), Y-Elim(4) 6. J(u), Y-Elim(4) 7. C(u), Y-Elim(4) 8. S(u,a), MPG(1,4) ={x/u}
9. E(u,b), MPG(2,5,7) ={x/u} 10. S(u,c), MPG(3,5,8,9) ={x/u}
Modus Ponens
Resolución { , } { , } ___________ { , }
________ Y-Eliminación
Eliminación universal
... ________
1
2
n
i
Y-Introducción ... n ________ 1 2 . . . n 1
2
O-Introducción 1
________ 1
x ________ SUST({x/g}, )
Eliminación existencial x ________ SUST({x/k}, )
Inferencia en lógica de predicados Modus ponens generalizado p1’ p2’ . . . pn’ (p1 p2 . . . pn q) ____________________________ SUST( ,q)
donde pi’ son términos base y pi son sentencias cuantificadas en las que existe una sustitución pi’=SUST( ,pi) para toda i
tal que
Inferencia en lógica de predicados Resolución generalizada p1 . . . pj . . . pm q1 . . . qj . . . qn __________________________________ SUST( , p1 . . . pj-1 pj+1. . . pm q1 . . . qj-1 qj+1. . . qn)
donde pi son términos base, qi son predicados cuantificados universalmente y existe una sustitución tal que unifiquen pj y qj
Inferencia en lógica de predicados Resolución generalizada p1 . . . pj . . . pm q1 . . . qj . . . qn __________________________________ SUST( , p1 . . . pj-1 pj+1. . . pm q1 . . . qj-1 qj+1. . . qn)
1. P(a) R(a) 2.
x
P(x) Q(x)
Inferencia en lógica de predicados Resolución generalizada p1 . . . pj . . . pm q1 . . . qj . . . qn __________________________________ SUST( , p1 . . . pj-1 pj+1. . . pm q1 . . . qj-1 qj+1. . . qn)
1. P(a) R(a) 2.
x
P(x) Q(x)
3.
P(a) Q(a), Elim-Universal(2)
={x/a}
Inferencia en lógica de predicados Resolución generalizada p1 . . . pj . . . pm q1 . . . qj . . . qn __________________________________ SUST( , p1 . . . pj-1 pj+1. . . pm q1 . . . qj-1 qj+1. . . qn)
1. P(a) R(a) 2.
x
P(x) Q(x)
3.
P(a) Q(a), Elim-Universal(2)
4. R(a) Q(a), res(1,3)
={x/a}
Inferencia en lógica de predicados Resolución generalizada p1 . . . pj . . . pm q1 . . . qj . . . qn __________________________________ SUST( , p1 . . . pj-1 pj+1. . . pm q1 . . . qj-1 qj+1. . . qn)
1. P(a) R(a) 2.
x
P(x) Q(x)
Inferencia en lógica de predicados Resolución generalizada p1 . . . pj . . . pm q1 . . . qj . . . qn __________________________________ SUST( , p1 . . . pj-1 pj+1. . . pm q1 . . . qj-1 qj+1. . . qn)
1. P(a) R(a) 2.
x
P(x) Q(x)
3. R(a) Q(a), RG(1,2)
={x/a}
Inferencia en lógica de predicados Resolución generalizada p1 . . . pj . . . pm q1 . . . qj . . . qn __________________________________ SUST( , p1 . . . pj-1 pj+1. . . pm q1 . . . qj-1 qj+1. . . qn)
donde pi son términos base, qi son predicados cuantificados universalmente y existe una sustitución tal que unifiquen pj y qj
Inferencia en lógica de predicados Forma normal conjuntiva
• Si cada una de las sentencias es una disyunción, se dice que están en forma normal conjuntiva
Inferencia en lógica de predicados Conversión a forma normal conjuntiva
Procedimiento para convertir una sentencia cualquiera a forma normal conjuntiva 1. Eliminar implicaciones 2. Empujar las negaciones
3. Eliminar cuantificadores existenciales
Inferencia en lógica de predicados Conversión a forma normal conjuntiva
Procedimiento para convertir una sentencia cualquiera a forma normal conjuntiva 1. Eliminar implicaciones p q
p q
2. Empujar las negaciones (p q)
p
q
(p q)
p
q
( p)
p
Inferencia en lógica de predicados 3. Eliminar los cuantificadores existenciales
Caso 1: un cuantificador existencial no está dentro del alcance de uno universal
Inferencia en lógica de predicados 3. Eliminar los cuantificadores existenciales
Caso 1: un cuantificador existencial no está dentro del alcance de uno universal
• y x P(x,y)Q(x,y)
El cuantificado existencial no está dentro del alcance de uno universal
x y P(x,y)Q(x,y)
El cuantificado existencial está dentro del alcance de uno universal
•
Inferencia en lógica de predicados 3. Eliminar los cuantificadores existenciales
Caso 1: un cuantificador existencial no está dentro del alcance de uno universal •
x P(x)
•
x y P(x) Q(y)
Inferencia en lógica de predicados 3. Eliminar los cuantificadores existenciales
Caso 1: un cuantificador existencial no está dentro del alcance de uno universal •
x P(x)
•
x y P(x) Q(y) Se reemplaza la variable cuantificada existencialmente por una constante que no hace parte de BC
Inferencia en lógica de predicados 3. Eliminar los cuantificadores existenciales
Caso 1: un cuantificador existencial no está dentro del alcance de uno universal x P(x) quedaría como P(a) donde a es una constante que no está en BC x y P(x) Q(y) quedaría y P(a) Q(y), donde a es una constante que no está en BC Se reemplaza la variable cuantificada existencialmente por una constante que no hace parte de BC
Inferencia en lógica de predicados Caso 2: un cuantificador existencial está dentro del alcance de uno universal
Inferencia en lógica de predicados Caso 2: un cuantificador existencial está dentro del alcance de uno universal “Todos tenemos un corazón” x y Persona(x)
Corazon(y) Tiene(x,y)
Si se reemplaza y por una constante se tendría:
x Persona(x)
Corazon(H) Tiene(x,H)
Inferencia en lógica de predicados Caso 2: un cuantificador existencial está dentro del alcance de uno universal “Todos tenemos un corazón” x y Persona(x)
Corazon(y) Tiene(x,y)
Si se reemplaza y por una constante se tendría:
x Persona(x)
Corazon(H) Tiene(x,H)
Lo que indica que todas las personas comparten el mismo corazón
Inferencia en lógica de predicados Caso 2: un cuantificador existencial está dentro del alcance de uno universal “Todos tenemos un corazón” x y Persona(x)
Corazon(y) Tiene(x,y)
Si se reemplaza y por una constante se tendría:
x Persona(x) •
Corazon(H) Tiene(x,H)
Para indicar que cada persona tiene su propio corazón se incorpora una función
Inferencia en lógica de predicados Caso 2: un cuantificador existencial está dentro del alcance de uno universal x y Persona(x)
x Persona(x)
Corazon(y) Tiene(x,y)
Corazon(f(x)) Tiene(x,f(x))
Se reemplaza la variable cuantificada existencialmente por una función que depende de la variable cuantificada universalmente
1.
x y (E(y)
R(x,y))
2.
x y A(x)
(I(y)
3. x E(x) R(a,x) 4. M(a,b)
M(c,b)
5. G(b) 6.
x G(x)
I(x)
A(x)
M(x,y))
1.
x y (E(y)
R(x,y))
2.
x y A(x)
(I(y)
A(x)
M(x,y))
3. x E(x) R(a,x) 4. M(a,b)
M(c,b)
5. G(b) 6.
x G(x)
I(x)
1. Eliminar implicaciones
1.
x y (E(y)
R(x,y))
2.
x y A(x)
(I(y)
A(x)
M(x,y))
3. x E(x) R(a,x) 4. M(a,b)
M(c,b)
5. G(b) 6.
x G(x)
I(x)
1. Eliminar implicaciones 1.
x y
(E(y)
R(x,y))
2.
x y
A(x)
( I(y)
3. x E(x) R(a,x) 4. M(a,b)
M(c,b)
5. G(b) 6.
x
G(x)
I(x)
A(x)
M(x,y))
1.
x y
(E(y)
R(x,y))
2.
x y
A(x)
( I(y)
A(x)
3. x E(x) R(a,x)
4. M(a,b)
M(c,b)
5. G(b) 6.
x
G(x)
I(x)
2. Empujar negaciones
M(x,y))
1.
x y
(E(y)
R(x,y))
2.
x y
A(x)
( I(y)
A(x) M(x,y))
3. x E(x) R(a,x)
4. M(a,b)
M(c,b)
5. G(b) 6.
x
G(x)
I(x)
2. Empujar negaciones 1.
x y
E(y)
R(x,y)
2.
x y
A(x)
I(y)
3. x E(x) R(a,x) 4. M(a,b)
M(c,b)
5. G(b) 6.
x
G(x)
I(x)
A(x)
M(x,y)
1.
x y
E(y)
R(x,y)
2.
x y
A(x)
I(y)
A(x)
M(x,y)
3. x E(x) R(a,x) 4. M(a,b)
M(c,b)
5. G(b) 6.
x
G(x)
I(x)
3. Eliminar cuantificadores existenciales
1.
x y
E(y)
R(x,y)
2.
x y
A(x)
I(y)
A(x)
M(x,y)
3. x E(x) R(a,x) 4. M(a,b)
M(c,b)
5. G(b) 6.
x
G(x)
I(x)
3. Eliminar cuantificadores existenciales 1.
E(f(x))
R(x,f(x))
A(x)
1.
x y
E(y)
R(x,y)
2.
x y
A(x)
I(y)
A(x)
M(x,y)
3. x E(x) R(a,x) 4. M(a,b)
M(c,b)
5. G(b) 6.
x
G(x)
I(x)
3. Eliminar cuantificadores existenciales 1.
E(f(x))
2.
A(x)
R(x,f(x)) I(y)
A(x)
M(x,y)
1.
x y
E(y)
R(x,y)
2.
x y
A(x)
I(y)
A(x)
M(x,y)
3. x E(x) R(a,x) 4. M(a,b)
M(c,b)
5. G(b) 6.
x
G(x)
I(x)
3. Eliminar cuantificadores existenciales 1.
E(f(x))
2.
A(x)
R(x,f(x)) I(y)
3. E(d) R(a,d)
A(x)
M(x,y)
1.
x y
E(y)
R(x,y)
2.
x y
A(x)
I(y)
A(x)
M(x,y)
3. x E(x) R(a,x) 4. M(a,b)
M(c,b)
5. G(b) 6.
x
G(x)
I(x)
3. Eliminar cuantificadores existenciales 1.
E(f(x))
2.
A(x)
R(x,f(x)) I(y)
3. E(d) R(a,d) 4. M(a,b)
M(c,b)
5. G(b)
6.
G(x)
I(x)
A(x)
M(x,y)
1.
E(f(x))
2.
A(x)
R(x,f(x)) I(y)
A(x)
M(x,y)
3. E(d) R(a,d)
4. M(a,b)
M(c,b)
5. G(b) 6.
G(x)
I(x)
Representar en forma de conjuntos
1.
E(f(x))
2.
A(x)
R(x,f(x)) I(y)
A(x)
M(x,y)
3. E(d) R(a,d)
4. M(a,b)
M(c,b)
5. G(b) 6.
G(x)
I(x)
Representar en forma de conjuntos 1. { E(f(x)) , 2. { A(x) ,
R(x,f(x)) , A(x)}
I(y) ,
3. {E(d)} 4. {R(a,d)} 5. {M(a,b) , M(c,b)}
6. {G(b)} 7. { G(x) , I(x)}
M(x,y)}
1. { E(f(x)) , 2. { A(x) ,
R(x,f(x)) , A(x)}
I(y) ,
M(x,y)}
3. { G(x) , I(x)}
4. {E(d)} 5. {R(a,d)} 6. {M(a,b) , M(c,b)}
7. {G(b)}
Demostrar por contradicción M(c,b)
1. { E(f(x)) , 2. { A(x) ,
R(x,f(x)) , A(x)}
I(y) ,
M(x,y)}
3. { G(x) , I(x)}
4. {E(d)} 5. {R(a,d)} 6. {M(a,b) , M(c,b)}
7. {G(b)} 8. { M(c,b)}
Demostrar por contradicción M(c,b)
1. { E(f(x)) , 2. { A(x) ,
R(x,f(x)) , A(x)}
I(y) ,
3. { G(x) , I(x)}
4. {E(d)} 5. {R(a,d)} 6. {M(a,b) , M(c,b)}
7. {G(b)} 8. { M(c,b)}
M(x,y)}
1. { E(f(x)) , 2. { A(x) ,
R(x,f(x)) , A(x)}
I(y) ,
M(x,y)}
3. { G(x) , I(x)}
4. {E(d)} 5. {R(a,d)} 6. {M(a,b) , M(c,b)}
7. {G(b)} 8. { M(c,b)} 9. { R(x,d), A(x)}
RG(1,4) ={f(x)/d}
1. { E(f(x)) , 2. { A(x) ,
R(x,f(x)) , A(x)}
I(y) ,
M(x,y)}
3. { G(x) , I(x)}
4. {E(d)} 5. {R(a,d)} 6. {M(a,b) , M(c,b)}
7. {G(b)} 8. { M(c,b)} 9. { R(x,d), A(x)}
RG(1,4) ={f(x)/d}
10. {A(a)}
RG(5,9), ={x/a}
1. { E(f(x)) , 2. { A(x) ,
R(x,f(x)) , A(x)}
I(y) ,
M(x,y)}
3. { G(x) , I(x)}
4. {E(d)} 5. {R(a,d)} 6. {M(a,b) , M(c,b)}
7. {G(b)} 8. { M(c,b)} 9. { R(x,d), A(x)}
RG(1,4) ={f(x)/d}
10. {A(a)}
RG(5,9), ={x/a}
11. {I(b)}
RG(3,7), ={x/b}
1. { E(f(x)) , 2. { A(x) ,
R(x,f(x)) , A(x)}
I(y) ,
M(x,y)}
3. { G(x) , I(x)}
4. {E(d)} 5. {R(a,d)} 6. {M(a,b) , M(c,b)}
7. {G(b)} 8. { M(c,b)} 9. { R(x,d), A(x)}
RG(1,4) ={f(x)/d}
10. {A(a)}
RG(5,9), ={x/a}
11. {I(b)}
RG(3,7), ={x/b}
12. { A(x),
M(x,b)}
RG(2,11), ={y/b}
1. { E(f(x)) , 2. { A(x) ,
R(x,f(x)) , A(x)}
I(y) ,
M(x,y)}
3. { G(x) , I(x)}
4. {E(d)} 5. {R(a,d)} 6. {M(a,b) , M(c,b)}
7. {G(b)} 8. { M(c,b)} 9. { R(x,d), A(x)}
RG(1,4) ={f(x)/d}
10. {A(a)}
RG(5,9), ={x/a}
11. {I(b)}
RG(3,7), ={x/b}
12. { A(x), 13. { M(a,b)}
M(x,b)}
RG(2,11), ={y/b} RG(10,12), ={x/a}
1. { E(f(x)) , 2. { A(x) ,
R(x,f(x)) , A(x)}
I(y) ,
M(x,y)}
3. { G(x) , I(x)}
4. {E(d)} 5. {R(a,d)} 6. {M(a,b) , M(c,b)}
7. {G(b)} 8. { M(c,b)} 9. { R(x,d), A(x)}
RG(1,4) ={f(x)/d}
10. {A(a)}
RG(5,9), ={x/a}
11. {I(b)}
RG(3,7), ={x/b}
12. { A(x),
M(x,b)}
RG(2,11), ={y/b}
13. { M(a,b)}
RG(10,12), ={x/a}
14. {M(a,b)}
res(6,8)
1. { E(f(x)) , 2. { A(x) ,
R(x,f(x)) , A(x)}
I(y) ,
M(x,y)}
3. { G(x) , I(x)}
4. {E(d)} 5. {R(a,d)} 6. {M(a,b) , M(c,b)}
7. {G(b)} 8. { M(c,b)} 9. { R(x,d), A(x)}
RG(1,4) ={f(x)/d}
10. {A(a)}
RG(5,9), ={x/a}
11. {I(b)}
RG(3,7), ={x/b}
12. { A(x),
M(x,b)}
RG(2,11), ={y/b}
13. { M(a,b)}
RG(10,12), ={x/a}
14. {M(a,b)}
res(6,8)
15.
Y-Intro(13,14)
Inferencia en lógica de predicados • Convierta a forma normal conjuntiva y demuestre por contradicción R(a,b) T(a,b) 1. x y Q(x) R(y,x)
2.
x y P(x) T(x,y)
3.
P(a)
4. S(a)
S(x)
Inferencia en lógica de predicados • Convierta a forma normal conjuntiva y demuestre por contradicción R(a,b) T(a,b) 1. Q(b) R(y,b)
2. P(x) T(x,f(x)) 3.
P(a)
4. S(a)
S(x)
Inferencia en lógica de predicados • Convierta a forma normal conjuntiva y demuestre por contradicción R(a,b) T(a,b) 1. {Q(b) R(y,b)}
2. {P(x),T(x,f(x)), S(x)} 3. { P(a)} 4. {S(a)}
Inferencia en lógica de predicados • Convierta a forma normal conjuntiva y demuestre por contradicción R(a,b) T(a,b) 1. {Q(b) R(y,b)}
2. {P(x),T(x,f(x)), S(x)} 3. { P(a)} 4. {S(a)} 5. { R(a,b), T(a,b)}
Inferencia en lógica de predicados 1. {Q(b) R(y,b)} 2. {P(x),T(x,f(x)), S(x)}
3. { P(a)} 4. {S(a)} 5. { R(a,b), T(a,b)} 6. {Q(b)}, Y-Elim(1)
7. {R(y,b)}, Y-Elim(1) 8. { T(a,b)}, RG(5,7) ={y/a} 9. {P(a), S(a)}, RG(2,8) ={x/a, f(x)/b}
10. { S(a)}, res(3,9) 11.
, Y-Intro(4,10)
Inferencia en lógica de predicados • Convierta a forma normal conjuntiva y demuestre por contradicción T(b) 1. x y 2.
x y R(x,y)(T(y) P(y))
3. Q(b) 4.
R(x,y) Q(y)
P(b)
Inferencia en lógica de predicados • Convierta a forma normal conjuntiva y demuestre por contradicción T(b) 1. {R(a,y),
Q(y)}
2. { R(x,f(x)), T(f(x)), P(f(x))} 3. {Q(b)}
4. { P(b)} 5. { T(b)} 6. {R(a,b)}, RG(1,3) , ={y/b} 7. {T(b),P(b)}, RG(2,6) , ={x/a,f(x)/b}
8. {T(b)}, res(4,7) 9.
, Y-Intro(5,8)
Inferencia en lógica de predicados • Convierta a forma normal conjuntiva y demuestre por contradicción R(b) 1.
x y (P(x)
2. x y 3. x P(x) 4. S(a)
Q(x)
Q(y)) R(x)
S(y)
Inferencia en lógica de predicados • Convierta a forma normal conjuntiva y demuestre por contradicción R(b) 1. { P(x),Q(f(x)),R(x)}
2. { Q(b), S(y)} 3. {P(b)} 4. {S(a)}
Inferencia en lógica de predicados • Convierta a forma normal conjuntiva y demuestre por contradicción R(b) 1. { P(x),Q(f(x)),R(x)} 2. { Q(b), S(y)}
3. {P(b)} 4. {S(a)} 5. { R(b)}
6. { Q(b)}, RG(2,4) ={y/a} 7. { P(x),R(x)}, RG(1,6) ={f(x)/b} 8. {R(b)}, RG(3,7) ={x/b}
9.
, Y-Intro(5,8)
Inferencia en lógica de predicados • Convierta a forma normal conjuntiva y demuestre por contradicción G(a,d) 1.
x C(x)G(a,x)
2. C(f) 3. C(b)
4.
x y (P(x,y)
5. C(c,d) 6.
M(y,x))C(y)
M(d,c)
x P(c,x)P(e,x)
1. { C(x),G(a,x)}
2. {C(f)} 3. {C(b)} 4. { P(x,y),M(y,x),C(y)}
5. {P(c,d)} 6. { M(d,c)} 7. { P(c,x),P(e,x)} 8. { G(a,d)}
1. { C(x),G(a,x)}
2. {C(f)} 3. {C(b)} 4. { P(x,y),M(y,x),C(y)}
5. {P(c,d)} 6. { M(d,c)} 7. { P(c,x),P(e,x)} 8. { G(a,d)}
9. {M(d,c),C(d)}, RG(4,5) ={x/c, y/d} 10. {C(d)}, res(6,9) 11. {G(a,d)}, RG(1,10) ={x/d}
12.
, Y-Intro(8,11)