Probador de teoremas lógicos

Se ha sugerido que este artículo o sección sea fusionado en Demostración interactiva de teoremas y Demostración automática de teoremas.
Motivo: los argumentos están expuestos en la página de discusión.

Una vez que hayas realizado la fusión de contenidos, pide la fusión de historiales aquí.

Este aviso fue puesto el 3 de noviembre de 2022.

Un probador de teoremas lógicos es una metodología o programa (software), que rechaza o acepta un teorema según un conjunto de reglas predefinidas.^[1] Ejemplos: Prolog y el lenguaje Lisp creado por John McCarthy del MIT en 1958.^[2]

Referencias

↑ 2c0bi (20 de octubre de 2019). «2 del mejor software de razonamiento automatizado para una lógica simplificada». Mundowin. Consultado el 2 de noviembre de 2022.
↑ Teigens, Vasil; Skalfist, Peter; Mikelsten, Daniel. Inteligencia artificial: la cuarta revolución industrial. Cambridge Stanford Books. Consultado el 3 de noviembre de 2022.