La regla de resolución de inferencia con frecuencia se implanta en programas de inteligencia artificial para probar teoremas.

En realidad, la resolución es la principal regla de PROLOG. En lugar de muchas reglas de inferencia de aplicación limitada, como modus ponens, modus tollens, etcétera, PROLOG utiliza una regla de inferencia general de resolución.

Esta aplicación de la resolución hace que los probadores automáticos de teoremas como PROLOG resulten herramientas prácticas para resolver problemas, por que en lugar de tener que probar diferentes reglas de inferencia esperando que una tenga éxito, puede aplicarse la regla de resolución simple, método que puede reducir mucho el espacio de búsqueda.[2]

Las diferentes reglas que sirven para deducir formas simplificadas son las siguientes: