El presente es un curso avanzado de lógica para informáticos. De entre las distintas aplicaciones de la lógica en la informática, se pueden destacar, entre otras, las técnicas de verificación formal de programas, la programación lógica o la inteligencia artificial. Como complemento a los fundamentos teóricos del curso, se introduce el problema de la demostración automática de teoremas. Se presentan diferentes heurísticas para la demostración automática de teoremas, así como distintos sistemas implementados con los que comprobar la potencia de las técnicas expuestas. Los sistemas de demostración automática de teoremas resultan particularmente útiles en el desarrollo de métodos formales en la ingeniería del software.