Il s'agit de la commande mace2 qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks en utilisant l'un de nos multiples postes de travail en ligne gratuits tels que Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS
PROGRAMME:
Nom
mace2 - recherche des contre-modèles finis d'instructions du premier ordre
SYNOPSIS
mace2 [Options] fichier-entrée > fichier de sortie
DESCRIPTION
Cette page de manuel documente brièvement les mace2 commander.
mace2 est un programme qui recherche des modèles finis d'énoncés du premier ordre. Le
l'instruction à modéliser est d'abord traduite en clauses, puis en clauses relationnelles ;
enfin, pour la taille de domaine donnée, les instances terrain sont construites. Un Davis-Putnam-
La procédure de Loveland-Logeman résout le problème propositionnel, et tous les modèles trouvés sont
traduit en modèles de premier ordre. mace2 est un complément utile au prouveur de théorème
loutre(1), avec loutre chercher des preuves et mace2 à la recherche de contre-modèles.
OPTIONS
Un résumé des options est inclus ci-dessous.
-n n Cela donne la taille de domaine de départ pour la recherche. La valeur par défaut est 2. Si vous
donner aussi un -N option, MACE itérera la taille des domaines à travers le -N valeur.
Dans le cas contraire, mace2 recherchera uniquement le -n valeur.
-N n Cela donne la taille du domaine final pour la recherche. La valeur par défaut est la valeur du
-n option.
-c Cela signifie que les constantes de l'entrée doivent se voir attribuer des éléments uniques du
domaine. Si le nombre de constantes en entrée est supérieur à la taille du domaine n,
le premier n les constantes reçoivent des valeurs et le reste n'est pas contraint. C'est un
option utile car elle élimine beaucoup d’isomorphisme de la recherche. Mais ça peut
bloquer tous les modèles, en particulier lorsqu'ils sont utilisés avec d'autres contraintes.
-p Cette option indique mace2 pour imprimer les modèles sous une jolie forme tabulaire au fur et à mesure qu'ils sont trouvés.
Ce format est destiné à la consommation humaine.
-P Cette option indique mace2 pour imprimer des modèles sous une forme facilement analysable. Ce format a
an loutre-syntaxe similaire et peut être lu par la plupart des systèmes Prolog.
-I Cette option indique mace2 pour imprimer des modèles sous forme IVY. Ce format est un Lisp S-
expression et est destiné à être lu par IVY, notre vérificateur d’épreuves et de modèles.
-m n Cela raconte mace2 arrêter après avoir trouvé n des modèles. La valeur par défaut est 1.
-t n Cela raconte mace2 pour s'arrêter après environ n secondes. La valeur par défaut est illimitée. mace2
ne tient pas compte tous assigner(max_secondes, n) commandes qui pourrait be in le contribution fichier. Tel
commandes d'utiliser by loutre seulement.
-k n Cela raconte mace2 s'arrêter s'il essaie d'allouer plus que n kilo-octets de mémoire.
La valeur par défaut est 48000 48 (environ XNUMX mégaoctets). mace2 ne tient pas compte tous assigner(max_mem, n)
commandes qui pourrait be in le contribution fichier. Tel commandes d'utiliser by loutre seulement.
-x Il s'agit d'une contrainte spéciale conçue pour réduire l'isomorphisme dans les quasi-groupes
problèmes. Cela s'applique uniquement à la fonction binaire f.
-h Cela raconte mace2 pour imprimer un résumé de ces options de ligne de commande.
Utilisez mace2 en ligne en utilisant les services onworks.net
