Este é o comando mace2 que pode ser executado no provedor de hospedagem gratuita OnWorks usando uma de nossas várias estações de trabalho online gratuitas, como Ubuntu Online, Fedora Online, emulador online do Windows ou emulador online do MAC OS
PROGRAMA:
NOME
mace2 - procura por contra-modelos finitos de declarações de primeira ordem
SINOPSE
mace2 [opções] Arquivo de entrada > arquivo de saída
DESCRIÇÃO
Esta página de manual documenta resumidamente o mace2 comando.
mace2 é um programa que procura modelos finitos de declarações de primeira ordem. o
a instrução a ser modelada é primeiro traduzida em cláusulas e, em seguida, em cláusulas relacionais;
finalmente, para o tamanho de domínio dado, as instâncias básicas são construídas. A Davis-Putnam-
O procedimento de Loveland-Logeman decide o problema proposicional, e quaisquer modelos encontrados são
traduzido para modelos de primeira ordem. mace2 é um complemento útil para o provador de teoremas
lontra(1), com lontra procurando por provas e mace2 procurando por contra-modelos.
OPÇÕES
Um resumo das opções está incluído abaixo.
-n n Isso fornece o tamanho do domínio inicial para a pesquisa. O valor padrão é 2. Se você
também dê um -N opção, o MACE irá iterar os tamanhos de domínio até o -N valor.
Caso contrário, mace2 irá procurar apenas pelo -n valor.
-N n Isso fornece o tamanho do domínio final para a pesquisa. O padrão é o valor do
-n opção.
-c Isso diz que as constantes na entrada devem receber elementos únicos do
domínio. Se o número de constantes na entrada for maior que o tamanho do domínio n,
o primeiro n constantes recebem valores e o resto é irrestrito. Isto é um
opção útil porque elimina muito isomorfismo da pesquisa. Mas pode
bloquear todos os modelos, especialmente quando usados com outras restrições.
-p Esta opção diz mace2 para imprimir modelos em uma bela forma tabular à medida que são encontrados.
Este formato é destinado ao consumo humano.
-P Esta opção diz mace2 para imprimir modelos de uma forma facilmente analisável. Este formato tem
an lontrasemelhante à sintaxe e pode ser lida pela maioria dos sistemas Prolog.
-I Esta opção diz mace2 para imprimir modelos no formato IVY. Este formato é um Lisp S-
expressão e deve ser lido por IVY, nosso verificador de provas e modelos.
-m n Isso diz mace2 parar depois de encontrar n modelos. O padrão é 1.
-t n Isso diz mace2 para parar após cerca de n segundos. O padrão é ilimitado. mace2
ignora qualquer atribuir (max_segundos, n) comandos que poder be in da entrada arquivo. Tal
comandos e guarante que os mesmos estão usava by lontra só.
-k n Isso diz mace2 parar se tentar alocar mais de n kilobytes de memória.
O padrão é 48000 (cerca de 48 megabytes). mace2 ignora qualquer atribuir (max_mem, n)
comandos que poder be in da entrada arquivo. Tal comandos e guarante que os mesmos estão usava by lontra só.
-x Esta é uma restrição de propósito especial projetada para reduzir o isomorfismo em quase-grupos
problemas. Aplica-se apenas à função binária f.
-h Isso diz mace2 para imprimir um resumo dessas opções de linha de comando.
Use mace2 online usando serviços onworks.net
