El objetivo del artículo es el estudio de los fundamentos lógicos que están en la base de gran cantidad de sistemas de razonamiento automático, y que suponen una estrategia computacionalmente viable para la demostración de teoremas o el diseño de motores inferenciales (Prolog). En concreto se presenta la forma clausal. en tanto que formalismo para la representación de conocimiento, y el principio de resolución, como mecanismo inferencia! que asegura la completud y corrección lógicas.
