siguiente arriba atrasadelante (solo si previamente se ha ido atras)

4.6.1. Reglas de inferencia

Las reglas definidas en el Apartado 3.6.1 eran: modus ponens, modus ponens, introducción y eliminación de conjunción, encadenamiento y resolución. Todas ellas son aplicables, en su forma general, a la lógica de predicados. Pero ahora hemos que tener en cuenta que las sentencias que figuran en ellas contienen, en lugar de variables proposicionales, átomos (predicados con términos como argumentos), lo que complica la aplicación de las reglas. Hay una regla de inferencia específica para la lógica de predicados, que generalmente es necesaria para poder aplicar cualquiera de las otras:

La regla de particularización de un universal permite razonar de lo general a lo particular:

P: ( A x)(f(x))

C: f(A)

Está basada en |=(( A x)(f(x)) ==> f(A)), donde f(x) representa una sentencia que contiene la variable libre x, y f(A) es la misma sentencia en la que x se ha sustituido por una constante.

Enseguida veremos que efectivamente se aplica en las demostraciones (de manera intuitiva cuando las demostraciones las hacemos mentalmente). En el modelo procesal de Prolog (Apartado A.3.2) ésta es la regla que se aplica cuando se sustituye una variable por una constante para unificar (o «ejemplarizar» ).


siguiente arriba atrasadelante (sólo si previamente se ha ido atras)

algunos derechos reservados DIT-ETSIT-UPM
Portada