Tarea 7: Aplicación de la Lógica Predicativa

La aplicación de la lógica predicativa que utilizaré de ejemplo será la Prueba de Teoremas.

"Un teorema es una afirmación que puede ser demostrada dentro de un sistema formal."

Para probar teoremas podemos expresar el teorema en lógica de primer orden, es decir pasando los términos a predicados.

Buscando información por Internet encontré un applet MUY interesante que sirve para probar teoremas, expresándolos en un lenguaje especial muy similar a la programación.

Ejemplo 1:

Si queremos probar el teorema: "Emmanuel es mortal", solo sabiendo que los humanos son mortales, y que Emmanuel es un humano, podemos hacer lo siguiente:

Axiomas

1. Los humanos son mortales.
2. Emmanuel es un humano.

Teorema

• Emmanuel es mortal.

Lógica Predicativa

Expresión	Símbología
X es humano	Humano(X)
X es mortal	Mortal(X)

  1. x( Humano(x) → Mortal(x))
  (Para todo x, Sí x es humano entonces x es mortal)

  2. Humano(Emmanuel)

  (Emmanuel es humano)

Ahora con lo anterior, reemplazando x por Emmanuel en la primera, podemos concluir:

  Humano(Emmanuel) → Mortal(Emmanuel)
  (Si Emmanuel es Humano, Emmanuel es Mortal)

Como ya habíamos definido anteriormente que Emmanuel es humano, entonces la expresión se hace verdadera y se comprueba que Emmanuel es Mortal.

Utilizando la applet produce el siguiente resultado:

Ejemplo 2:

Si deseáramos probar que los monos son seres vivos, solo sabiendo son mamíferos, y que los mamíferos son seres vivos, podríamos hacer algo así:

Axiomas:

1. Los monos son mamíferos.
2. Los mamíferos son Seres Vivos.

Teorema

Los monos son Mamíferos

Lógica de Predicados

Expresión	Símbología
X es mamífero	Mamifero(X)
X es ser vivo	SerVivo(X)

  1. Mamifero(Monos)
  (Los monos son mamiferos)

  2. x( Mamifero(x) → SerVivo(x))
  (Para todo x, Sí x es un mamífero x es un ser vivo )

Con lo anterior, podemos concluir:

 Mamífero(Monos)  → SerVivo(Monos)
 (Sí los monos son mamíferos, los monos son seres vivos)

Y como ya habíamos concluido que los monos son mamíferos, se comprueba que los monos son seres vivos.

Aquí una captura de como lo resuelve el applet:

Referencias:

http://www.foundalis.com/mat/atp/Prover.html
http://en.wikipedia.org/wiki/First-order_logic