Probador de teoremas lógicos
De Wikipedia, la enciclopedia encyclopedia
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]
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. |