Modelos y contraejemplos

Modelos y Contraejemplos ( Mace ) es un buscador de modelos . ^{[ 1 ]} La mayoría de los demostradores automáticos de teoremas intentan realizar una prueba por refutación en la forma normal de cláusulas del problema de prueba, mostrando que la combinación de axiomas y conjetura negada nunca puede ser simultáneamente verdadera, es decir, no tiene un modelo. Un buscador de modelos como Mace, por otro lado, intenta encontrar un modelo explícito de un conjunto de cláusulas. Si tiene éxito, esto corresponde a un contraejemplo para la conjetura, es decir, refuta el teorema (afirmado).

Mace tiene licencia GNU GPL . ^{[ 2 ]}

• Nutria (demostrador de teoremas)
• Proverbio 9

• Descarga del sistema