Mace significa " Modelos y contraejemplos " y es un buscador de modelos . [1] La mayoría de los probadores de teoremas automatizados intentan realizar una demostración por refutación en la forma normal de la cláusula 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 de la conjetura, es decir, refuta el teorema (reivindicado).
Mace tiene licencia GNU GPL . [2]
Ver también
Referencias
- ^ Sitio de inicio de William McCune
- ^ Consulte el archivo COPIA en el tarball .