Las reglas de inferencia que se utilizan en la lógica proposicional son Modus Ponens, Y-Introducción, O-Introducción y Resolución. También son válidas en el caso de la lógica de primer orden.
Para manejar oraciones de lógica de primer orden con cuantificadores se adicionan tres reglas, las cuales son más complejas puesto que trata de sustituir entes particularres por variables.
Estas reglas son:
Eliminación universal
Eliminación existencial
Introducción existencial
Para todas las oraciones atómicas pi, pi' y q, en las que existe una situación q tal que SUST(q,pi') = SUST(q,pi) para toda i. (SUST(q,pi') es el resultado de aplicar la sustitución).
Para esta regla hay n+1 premisas: las n oraciones atómicas pi' y una implicación.
El Modus Ponens generalizado es una regla de inferencia eficiente por tres razones:
Sus pasos son más globales.
Los pasos que realiza son sensatos, donde utiliza sustituciones que garantizan su utilidad. El algoritmo de Unificación utiliza dos oraciones y produce una sustitución mediante la que las oraciones anteriores resultan idénticas.
Consta de un paso de compilación previa mediante el que todas las oraciones de la base de conocimientos se convierten a una forma canónica.
Forma Canónica: esta determina que cada oración de la base de conocimientos sea una oración atómica. A este tipo de oraciones se les denomina Horn.
Unificación: convierte dos oraciones p y q en una sustitución mediante la que p y q resultan idénticas.
UNIFICAR(p,q) = q donde SUST(q,p) = SUST(q,q)
q se conoce como el unificador de dos oraciones. UNIFICAR debe producir el unificador más general (o UMG) que es la sustitución con la mínima implicación del enlace de las variables.
La regla del Modus Ponens generalizado se puede utillizar de dos formas.
Encadenamiento hacia adelante: comenzar por la oraciones que están en la base de conocimientos y generar nuevas conclusiones. Se utiliza cuando se incorpora en la base de datos un nuevo hecho.
Encadenamiento hacia atrás: empezar por algo que queremos demostrar, donde se buscan las oraciones que nos permitan llegar a determinada conclusión, y por último tratar de establecer las premisas correspondientes. Se utiliza cuando es necesario demostrar una meta.
Un procedimiento de demostración donde se utilice Modus Pnones es incompleto ya que hay oraciones implicadas por la base de conocimientos que el procedimiento no puede inferir.
El matemático Gödel obtuvo resultados alentadores donde en su teorema de completez demostró que, en la lógica de primer orden, toda oración implicada a partir de cualquier conjunto de oraciones puede ser demostrada a partir de éste. Es decir, que se puede encontrar reglas de inferencia en las que es factible un procedimiento de demostración completo R.
La vinculación en la lógica de primer orden es semidecidible, es decir, podemos demostrar que las oraciones se deducen de las premisas, si este es el caso, pero lo que no siempre podemos demostrar es que no es así.
La consistencia de un conjunto de oraciones es también semidecidible.
El Modus Ponens no nos permite deducir nuevas implicaciones, sólo deduce conclusiones atómicas. La regla de resolución tiene más capacidad que el Modus Ponens.
La regla de inferencia de resolución generalizada constituye un completo sistema de demostración por refutación.
Resolución generalizada (disyunción): para las literales pi y qi, en donde UNIFICAR (pj, ¬qk) = q. De manera similar, es posible expresar lo anterior mediante implicaciones.
Resolución generalizada (implicaciones): para los átomos pi, qi, ri, si, en donde UNIFICAR (pj, qk) = q
Formas canónicas de resolución:
Cada una de las reglas es una disyunción de literales. Todas las disyunciones se agrupan en una conjunción implicita grande, por lo que a esta forma se le denomina Forma Normal Conjuntiva (FNC).
Cada una de las oraciones es una implicación con una conjunción de átomos a la izquierda y una disyunción de átomos a la derecha, a esto se lo conoce como Forma Implicativa Normal (FNI).
Es importante tener en cuenta que la resolución es una forma generalizada de Modus Ponens.
Pruebas de resolución: se pueden usar tanto en el encadenamiento hacia adelante como en el encadenamiento hacia atrás.
Técnicamente, el solvente final sería Verdad => S(A) v S(A), pero se elimino el disyuntivo reduntante, para efectuar esto se cuenta con una regla de inferencia denominada Factorización.
No obstante que encadenamiento con resolución es más poderoso que el encadenamiento con Modus Ponens, todavía esta incompleto.
Existe un procedimiento de inferencia completo en el que se utiliza la resolución conocida como Refutación, o también Demostración por Contradicción. Consiste que para demostrar P, supone que P es falsa y se demuestra una contradicción. Si esto es posible de hacer, entonces la BC debe implicar P, es decir:
(KB /\ ¬P => Falso) <=> (KB => P)
Conversión a la forma normal: cualquier oración lógica de primer orden se puede expresar en forma normal implicativa (o conjuntiva). El procedimiento para hacer la conversión a la forma normal paso a paso es:
Eliminar implicaciones.
Transferir adentro a ¬.
Normalizar las variables.
Desplazar los cuantificadores a la izquierda.
Eskolemice: es un procedimiento que consiste en remover los cuantifacadores existenciales mediante su eliminación.
Distribuir /\ en V.
Simplificar las conjunciones y disyunciones anidadas.
Convertir las disyuntivas en implicaciones.
La unificación es muy útil para cotejar variables y otros términos. El problema es que la unificación realiza una prueba sintáctica basándose en el aspecto de los términos de argumento, y no una verdadera prueba semántica basada en los objetos que tales término representan.
Una forma de resolver lo anterior es axiomatizando la igualdad, escribiendo sus propiedades. Es necesario aclarar que la igualdad es reflexiva, simétrica y transitiva y también que permite sustituir iguales por iguales en el caso de cualquier predicado o función.
La otra forma de manejar la desigualdad es mediante una regla de inferencia especial. La regla de Demodulación parte de la aseveración de igualdad x = y, y toda oración con un término anidado que unifique con x y derive la misma oración al sustituir y por el término anidado.
Existe una regla más potente, la Paramodulación, que se aplica al caso cuando no sabemos que x = y, pero si sabemos que, por ejemplo, x = y /\ P(x).
Preferenacia por la unidad: en esta estrategia es preferible efectuar resoluciones donde una de las oraciones es una sola literal (también conocida como cláusula unitaria).
Conjunto de apoyo: empieza por identificar un subconjunto de las oraciones denominadas como conjunto de apoyo. En todas las resoluciones se combina una oración del conjunto de apoyo con otra oración, y el resolutivo se añade al conjunto de apoyo. Si el conjunto de apoyo es pequeño comparado con toda la base de conocimientos, lo anterior reducirá de manera notable el espacio de búsqueda.
Resolución de entrada: cada una de las resoluciones se combina con una de las oraciones de entrada. La estrategia de la resolución lineal es una cierta generalización que permite resolver conjuntamente P y Q, sea que P forme parte de BC original o que P sea ancestro de Q en el árbol de demostración. La resolución lineal es completa.
Subsuposición: es un método que elimina todas aquellas oraciones subasumidas por uan oración que ya está presente en la BC.
