Reglas de inferencia

1. modus ponens o eliminación de la implicación
   
2. eliminación de and
   
3. introducción de and
   
4. introducción de or
   
5. eliminación de la doble negación
   
6. resolución unitaria
   
7. resolución
   
   o de forma equivalente
   

• todas las reglas de inferencia anteriores son sound
• prueba: secuencia de aplicaciones de regla de inferencia, comenzando por las sentencias que originalmente están en la KB y culminando en la generación de la sentencia cuya prueba se desea