این دستور mace2 است که می تواند در ارائه دهنده میزبانی رایگان OnWorks با استفاده از یکی از چندین ایستگاه کاری آنلاین رایگان ما مانند Ubuntu Online، Fedora Online، شبیه ساز آنلاین ویندوز یا شبیه ساز آنلاین MAC OS اجرا شود.
برنامه:
نام
mace2 - به دنبال مدل های متقابل متناهی از عبارات مرتبه اول است
خلاصه
گرز2 [گزینه های] فایل ورودی > فایل خروجی
شرح
این صفحه راهنما به اختصار مستندات گرز2 فرمان
گرز2 برنامه ای است که به جستجوی مدل های محدود عبارات مرتبه اول می پردازد. در
عبارتی که باید مدل‌سازی شود ابتدا به جملات و سپس به بندهای رابطه‌ای ترجمه می‌شود.
در نهایت برای اندازه دامنه داده شده، نمونه های زمینی ساخته می شوند. دیویس-پاتنام-
رویه Loveland-Logeman مسئله گزاره ای را تعیین می کند، و هر مدلی که یافت می شود
به مدل های درجه اول ترجمه شده است. گرز2 مکمل مفیدی برای اثبات قضیه است
سمور(1) ، با سمور جست و جوی شواهد و گرز2 به دنبال مدل های متقابل
OPTIONS
خلاصه ای از گزینه ها در زیر آمده است.
-n n این اندازه دامنه شروع را برای جستجو می دهد. مقدار پیش فرض 2 است. اگر شما
همچنین یک -N گزینه، MACE اندازه دامنه را از طریق آن تکرار می کند -N ارزش.
در غیر این صورت، گرز2 فقط برای جستجو خواهد شد -n ارزش.
-N n این به اندازه دامنه پایانی برای جستجو می دهد. پیش فرض مقدار the است
-n گزینه.
-c این می گوید که ثابت ها در ورودی باید به عناصر منحصر به فردی از آن اختصاص داده شوند
دامنه. اگر تعداد ثابت های ورودی بیشتر از اندازه دامنه باشد n,
اول n به ثابت ها مقادیر داده می شود و بقیه بدون محدودیت هستند. این یک است
گزینه مفیدی است زیرا بسیاری از ایزومورفیسم ها را از جستجو حذف می کند. اما می تواند
همه مدل ها را مسدود می کند، به خصوص زمانی که با محدودیت های دیگر استفاده می شود.
-p این گزینه می گوید گرز2 برای چاپ مدل ها به شکل جدولی زیبا همانطور که پیدا می شوند.
این قالب برای مصرف انسان در نظر گرفته شده است.
-P این گزینه می گوید گرز2 برای چاپ مدل ها به شکلی که به راحتی قابل تجزیه هستند. این فرمت دارد
an سمور-مانند نحو و توسط اکثر سیستم های Prolog قابل خواندن است.
-I این گزینه می گوید گرز2 برای چاپ مدل ها به صورت IVY. این فرمت Lisp S- است
بیان و قرار است توسط IVY، اثبات و مدل بررسی کننده ما خوانده شود.
-m n این می گوید گرز2 پس از یافتن متوقف شود n مدل ها. پیش فرض 1 است.
-t n این می گوید گرز2 پس از حدود n ثانیه متوقف شود. پیش فرض نامحدود است. گرز2
نادیده گرفته می شود هر اختصاص (حداکثر_ثانیه، n) دستورات که قدرت be in la ورودی فایل. چنین
دستورات هستند استفاده by سمور تنها.
-k n این می گوید گرز2 در صورت تلاش برای تخصیص بیش از n کیلوبایت حافظه
پیش فرض 48000 (حدود 48 مگابایت) است. گرز2 نادیده گرفته می شود هر assign(max_mem, n)
دستورات که قدرت be in la ورودی فایل. چنین دستورات هستند استفاده by سمور تنها.
-x این یک محدودیت با هدف ویژه است که برای کاهش ایزومورفیسم در شبه گروه طراحی شده است
چالش ها و مسائل. این فقط برای تابع باینری اعمال می شود f.
-h این می گوید گرز2 برای چاپ خلاصه ای از این گزینه های خط فرمان.
از mace2 به صورت آنلاین با استفاده از خدمات onworks.net استفاده کنید
