Este curso es una introducción a la automatización del razonamiento a través de distintos sistemas (OTTER, MACE, PVS).