mace2 - Online nel cloud

PROGRAMMA:

NOME

mace2 - ricerca contromodelli finiti di affermazioni del primo ordine

SINOSSI

mace2 [Opzioni] file di input > file di uscita

DESCRIZIONE

Questa pagina di manuale documenta brevemente il mace2 comando.

mace2 è un programma che cerca modelli finiti di affermazioni del primo ordine. Il
l'istruzione da modellare viene prima tradotta in clausole, poi in clausole relazionali;
infine per la dimensione del dominio data, vengono costruite le istanze di base. Un Davis-Putnam-
La procedura Loveland-Logeman decide il problema proposizionale e tutti i modelli trovati sono
tradotti in modelli di primo ordine. mace2 è un utile complemento al dimostratore di teoremi
lontra(1), con lontra alla ricerca di prove e mace2 alla ricerca di contromodelli.

VERSIONI

Di seguito è riportato un riepilogo delle opzioni.

-n n Questo fornisce la dimensione iniziale del dominio per la ricerca. Il valore predefinito è 2. Se
dare anche un -N opzione, MACE itererà le dimensioni del dominio attraverso il -N valore.
Altrimenti, mace2 cercherà solo il -n valore.

-N n Fornisce la dimensione del dominio finale per la ricerca. Il valore predefinito è il valore di
-n opzione.

-c Ciò afferma che alle costanti nell'input dovrebbero essere assegnati elementi univoci dell'
dominio. Se il numero di costanti nell'input è maggiore della dimensione del dominio n,
il primo n alle costanti vengono assegnati valori e il resto non ha vincoli. Questo è un
opzione utile perché elimina molti isomorfismi dalla ricerca. Ma può
bloccare tutti i modelli, soprattutto se utilizzati con altri vincoli.

-p Questa opzione dice mace2 per stampare i modelli in una bella forma tabellare man mano che vengono trovati.
Questo formato è destinato al consumo umano.

-P Questa opzione dice mace2 per stampare modelli in una forma facilmente analizzabile. Questo formato ha
an lontra-simile alla sintassi e può essere letto dalla maggior parte dei sistemi Prolog.

-I Questa opzione dice mace2 per stampare modelli in formato IVY. Questo formato è un Lisp S-
espressione ed è pensata per essere letta da IVY, il nostro verificatore di prove e modelli.

-m n Questo dice mace2 fermarsi dopo aver trovato n modelli. Il valore predefinito è 1.

-t n Questo dice mace2 per fermarsi dopo circa n secondi. L'impostazione predefinita è illimitata. mace2
ignora in qualsiasi assegna(max_secondi, n) comandi che forza be in , il ingresso file. Tale
comandi sono utilizzato by lontra solo.

-k n Questo dice mace2 per fermarsi se tenta di allocare più di n kilobyte di memoria.
Il valore predefinito è 48000 (circa 48 megabyte). mace2 ignora in qualsiasi assegna(max_mem, n)
comandi che forza be in , il ingresso file. Tale comandi sono utilizzato by lontra solo.

-x Questo è un vincolo speciale progettato per ridurre l'isomorfismo nel quasigruppo
problemi. Si applica solo alla funzione binaria f.

-h Questo dice mace2 per stampare un riepilogo di queste opzioni della riga di comando.

Utilizzare mace2 online utilizzando i servizi onworks.net