cosas

Deducción natural
La derivación natural hace uso de varias reglas de inferencia.
Introduce conectiva
Elimina conectiva
Nombre Regla
Nombre Regla
Teorema de la deducción ¬E
¬I
¬¬A ⊢ A
Teorema de la deducción ⇒ E
⇒I
A,A ⇒ B ⊢ B
A,B ⊢ A ∧ B
∧I
∧E
A∧ B⊢A
A∧ B⊢B
∨I
∨E
Teorema de la deducción
A ⊢ B∨ A
⇔I
⇔E
A ⇔ B⊢A⇒ B
A ⇒ B,
A ⇔ B⊢B⇒ A
B⇒A⊢A⇒B
Existen dos reglas para cadaconectiva lógica, una para introducir la conectiva y otra para eliminarla.
Probar que P ∧ Q ⊢ ( P ∨ Q ) ∧ ( Q ∨ R )
1

( P ∧ Q)

2
3
4
5
6

P
Q
P∨ R
Q∨R

( P ∨ Q ) ∧ (Q ∨ R)

∧ E ,1
∧ E ,1
∨I , 2
∨ I ,3
∧ I , 4,5

Implementación del teorema de la deducción.
Tres reglas de la tabla hacen uso del teorema de deducción. ¬I , ⇒ I , ∨ E .
En todos los casos hay que crear unaderivación subordinada y en el caso de ∨ E dos derivaciones
subordinadas.
Las subderivaciones pueden ser anidadas.
La derivación que crea la subderivación es la derivación de llamada.
Todas las subderivaciones presentan un supuesto adicional que se desecha una vez que la subderivación está
terminada.
El siguiente ejemplo prueba el silogismo hipotético.
1
2

P⇒Q
Q⇒R

3
4
5
6
7
8

PP⇒Q
Q
Q⇒R
R
P⇒R

R,1
⇒ E , 3, 4
R,2
⇒ E , 5, 6
⇒ I,3− 7

1

Derivación del Modus Tollens en deducción natural.
1
2

P⇒Q
¬Q

3
4
5
6
7
8

P
P⇒Q
Q
¬Q
Q ∧ ¬Q
¬P

R,1
⇒ E , 3, 4
R,2
∧ I ,5, 6
¬I , 3 − 7

Derivación por el silogismo disyuntivo.
1
2

P∨Q
¬Q

3
4

P
P

5

Q

6
7
8
9
10

¬P
Q ∧ ¬Q
¬¬P
P
P

R,3

∧ I , 2,5
¬I , 6 − 7¬E ,8
∨ E ,1, 3 − 4,5 − 9

Resolución.
La prueba del teorema de resolución es un método para hacer derivaciones que tiene las siguientes
propiedades:
Las únicas expresiones que se permiten en la prueba del teorema de la resolución son disyunción de
literales. Una disyunción de literales se llama cláusula. Todas las expresiones deben ser cláusulas.
La resolución se ajusta al principio derefutación, que demuestra que la negación de la conclusión es
inconsistente con las premisas.
Hay esencialmente una sola regla de inferencia, la resolución.
Ejemplo del Modus Ponens:
Se puede expresar como: P, P ⇒ Q ⊨ Q ,
La negación de la conclusión se añade a las premisas: P, P ⇒ Q, ¬Q ,
Se debe demostrar que es imposible encontrar asignación alguna que pueda satisfacer todas esasproposiciones, es decir que las proposiciones son inconsistentes. Hay que convertir todas las expresiones en
disyunciones: P, ¬P ∨ Q, ¬Q .
Dos cláusulas se pueden resolver si y solo si contienen dos literales complementarios.
Dando origen a una nueva cláusula llamada resolverte.

2

Si los literales complementarios son P y ¬P se dice que la resolución radica en P.
Las cláusulas que dan origen alresolvente se llaman cláusulas padre.
El resolverte sobre P es la disyunción de todos los literales de las cláusulas padre, excepto P y ¬P se
omiten en el resolverte.
Hallar el resolverte de: P ∨ ¬Q ∨ R y ¬S ∨ Q .
Las dos cláusulas se pueden resolver sobre Q porque Q es negativa en la primera cláusula y positiva en
la segunda.
El resolverte es la disyunción de P ∨ R con ¬S , por lo tanto,P ∨ R ∨ ¬S

Se pueden tratar las cláusulas como conjuntos: C = A ∪ B − { P, ¬P}
Para probar el Modus Ponens se usan las siguientes derivaciones:
1. P

Premisa

2. ¬P ∨ Q

Premisa

3. ¬Q

Negación de la conclusión

4. Q

Resolvente de 1, 2

5. F

Resolvente de 3, 4

Para el silogismo hipotético se tiene:
1. ¬P ∨ Q

Premisa

2. ¬Q ∨ R

Premisa

3. P

Derivada de lanegación de la conclusión

4. ¬R

Derivada de la negación de la conclusión

5. Q

Resolvente de 1, 3

6. ¬Q

Resolvente de 2, 4

7. F

Resolvente de 5, 6

3

Se suele utilizar la resolución unitaria que consiste en que todas las resoluciones implican al menos una
cláusula unitaria.
Otra estrategia es la del conjunto de apoyo:
Se dividen todas las cláusulas en dos...