Tipo de recurso
Software PLN y RI
Descripción
Sistema de detección automático para demostrar teoremas indicados en la lógica de primer orden con la igualdad. Codificado en ANSI C, es portable, fácil de instalar y rápido. Usado sobre todo en sistemas Unix, aunque algunas versiones limitadas funcionan en Windows. Uso libre sin restricción.
Enlace