Este es el comando mace2 que se puede ejecutar en el proveedor de alojamiento gratuito de OnWorks utilizando una de nuestras múltiples estaciones de trabajo en línea gratuitas, como Ubuntu Online, Fedora Online, emulador en línea de Windows o emulador en línea de MAC OS.
PROGRAMA:
NOMBRE
mace2: busca contramodelos finitos de declaraciones de primer orden
SINOPSIS
mace2 [opciones] fichero de entrada > archivo de salida
DESCRIPCIÓN
Esta página de manual documenta brevemente la mace2 mando.
mace2 es un programa que busca modelos finitos de declaraciones de primer orden. los
la declaración a modelar se traduce primero a cláusulas, luego a cláusulas relacionales;
finalmente, para el tamaño de dominio dado, se construyen las instancias terrestres. Un Davis-Putnam-
El procedimiento de Loveland-Logeman decide el problema proposicional, y los modelos encontrados son
traducido a modelos de primer orden. mace2 es un complemento útil para el demostrador de teoremas
nutria(1), con nutria buscando pruebas y mace2 buscando contramodelos.
OPCIONES
Un resumen de las opciones se incluye a continuación.
-n n Esto da el tamaño de dominio inicial para la búsqueda. El valor predeterminado es 2. Si
también da un -N opción, MACE iterará los tamaños de dominio a través de la -N .
De lo contrario, mace2 buscará solo el -n .
-N n Esto da el tamaño de dominio final para la búsqueda. El predeterminado es el valor de la
-n .
-c Esto dice que a las constantes en la entrada se les deben asignar elementos únicos del
dominio. Si el número de constantes en la entrada es mayor que el tamaño del dominio n,
la primera n a las constantes se les dan valores y el resto no están restringidos. Esto es un
opción útil porque elimina muchos isomorfismos de la búsqueda. Pero puede
bloquear todos los modelos, especialmente cuando se usa con otras restricciones.
-p Esta opción dice mace2 para imprimir modelos en una bonita forma tabular a medida que se encuentran.
Este formato está destinado al consumo humano.
-P Esta opción dice mace2 para imprimir modelos en una forma fácilmente analizable. Este formato tiene
an nutria-como sintaxis y puede ser leído por la mayoría de los sistemas Prolog.
-I Esta opción dice mace2 para imprimir modelos en formato IVY. Este formato es un Lisp S-
expresión y está destinado a ser leído por IVY, nuestro verificador de pruebas y modelos.
-m n Esto dice mace2 detenerse después de encontrar n modelos. El valor predeterminado es 1.
-t n Esto dice mace2 para detenerse después de unos n segundos. El valor predeterminado es ilimitado. mace2
ignora any asignar (max_seconds, n) comandos que puede be in los Las opciones de entrada archivo. Tal
comandos están usado by nutria solamente.
-k n Esto dice mace2 detenerse si intenta asignar más de n kilobytes de memoria.
El valor predeterminado es 48000 (aproximadamente 48 megabytes). mace2 ignora any asignar (max_mem, n)
comandos que puede be in los Las opciones de entrada archivo. Tal comandos están usado by nutria solamente.
-x Esta es una restricción de propósito especial diseñada para reducir el isomorfismo en cuasigrupo
problemas. Se aplica solo a la función binaria f.
-h Esto dice mace2 para imprimir un resumen de estas opciones de la línea de comandos.
Utilice mace2 en línea utilizando los servicios de onworks.net
