Ito ang command na mace2 na maaaring patakbuhin sa OnWorks na libreng hosting provider gamit ang isa sa aming maramihang libreng online na workstation gaya ng Ubuntu Online, Fedora Online, Windows online emulator o MAC OS online emulator
PROGRAMA:
NAME
mace2 - naghahanap ng mga may hangganang countermodel ng mga first-order na pahayag
SINOPSIS
tungkod2 [pagpipilian] input-file > output-file
DESCRIPTION
Ang manu-manong pahinang ito ay nagdodokumento ng maikling tungkod2 utos.
tungkod2 ay isang program na naghahanap ng mga may hangganang modelo ng mga first-order na pahayag. Ang
Ang pahayag na imodelo ay unang isinalin sa mga sugnay, pagkatapos ay sa mga ugnayang sugnay;
sa wakas para sa ibinigay na laki ng domain, ang mga ground instance ay binuo. Isang Davis-Putnam-
Ang pamamaraan ng Loveland-Logeman ay nagpapasya sa proposisyonal na problema, at anumang mga modelong natagpuan ay
isinalin sa mga first-order na modelo. tungkod2 ay isang kapaki-pakinabang na pandagdag sa theorem prover
otter(1), kasama ang otter naghahanap ng mga patunay at tungkod2 naghahanap ng mga countermodel.
Opsyon
Ang isang buod ng mga opsyon ay kasama sa ibaba.
-n n Nagbibigay ito ng panimulang laki ng domain para sa paghahanap. Ang default na halaga ay 2. Kung ikaw
magbigay din ng -N opsyon, uulitin ng MACE ang mga laki ng domain sa pamamagitan ng -N halaga.
Kung hindi, tungkod2 maghahanap lamang ng -n halaga.
-N n Nagbibigay ito ng panghuling laki ng domain para sa paghahanap. Ang default ay ang halaga ng
-n pagpipilian.
-c Sinasabi nito na ang mga constant sa input ay dapat magtalaga ng mga natatanging elemento ng
domain. Kung ang bilang ng mga constant sa input ay mas malaki kaysa sa laki ng domain n,
ang unang n ang mga constant ay binibigyan ng mga halaga, at ang natitira ay hindi pinipigilan. Ito ay
kapaki-pakinabang na opsyon dahil inaalis nito ang maraming isomorphism mula sa paghahanap. Pero pwede
harangan ang lahat ng mga modelo, lalo na kapag ginamit sa iba pang mga hadlang.
-p Ang pagpipiliang ito ay nagsasabi tungkod2 upang mag-print ng mga modelo sa magandang tabular na anyo habang sila ay matatagpuan.
Ang format na ito ay para sa pagkonsumo ng tao.
-P Ang pagpipiliang ito ay nagsasabi tungkod2 upang mag-print ng mga modelo sa isang madaling ma-parse na anyo. Ang format na ito ay may
an otter-tulad ng syntax at maaaring basahin ng karamihan sa mga sistema ng Prolog.
-I Ang pagpipiliang ito ay nagsasabi tungkod2 upang mag-print ng mga modelo sa IVY form. Ang format na ito ay Lisp S-
expression at nilalayong basahin ng IVY, ang aming patunay at tagasuri ng modelo.
-m n Sinasabi nito tungkod2 huminto pagkatapos mahanap n mga modelo. Ang default ay 1.
-t n Sinasabi nito tungkod2 huminto pagkatapos ng halos n segundo. Ang default ay walang limitasyon. tungkod2
binabalewala anumang italaga(max_seconds, n) utos na maaari be in ang input file. Ang nasabing
utos ay ginamit by otter lamang.
-k n Sinasabi nito tungkod2 na huminto kung sinusubukan nitong maglaan ng higit sa n kilobytes ng memorya.
Ang default ay 48000 (mga 48 megabytes). tungkod2 binabalewala anumang italaga(max_mem, n)
utos na maaari be in ang input file. Ang nasabing utos ay ginamit by otter lamang.
-x Ito ay isang espesyal na layunin na hadlang na idinisenyo upang bawasan ang isomorphism sa quasigroup
mga problema. Nalalapat lamang ito sa binary function f.
-h Sinasabi nito tungkod2 upang mag-print ng buod ng mga opsyon sa command-line na ito.
Gumamit ng mace2 online gamit ang mga serbisyo ng onworks.net
