FLOTTER - على الإنترنت في السحابة

برنامج:

اسم

SPASS - مبرهنة نظرية آلية لمنطق كامل من الدرجة الأولى مع المساواة

موجز

سباس [الخيارات] [ملف الإدخال]

الوصف

SPASS هو مُثبِّت نظرية آلية لمنطق كامل مرتبة من الدرجة الأولى مع المساواة التي
يوسع التراكب حسب النوع وقاعدة التجزئة لتحليل الحالة. يمكن أن يكون SPASS أيضًا
تستخدم كمنطق مشروط ومثبت نظرية منطق الوصف.

OPTIONS

يتم تنفيذ خيارات سطر الأوامر في SPASS عبر تعديلات على سطر أوامر GNU
حزمة الخيارات لـ C. مجرد إعطاء الخيار يضبط قيمته على 1 ويعني تمكين
خيار. لتعطيل خيار ما ، يجب ضبط القيمة على 0 بالتصريح -خيار= 0.
الخيارات التالية مدعومة حاليًا بواسطة SPASS:

-تلقاءي
يمكّن / يعطل الوضع التلقائي حيث يقوم SPASS بتكوين نفسه تلقائيًا. ال
قواعد الاستدلال / التخفيض ، تقنية الفرز ، الترتيب والأسبقية وكذلك
تم تعيين استراتيجية التقسيم والاختيار. في الوضع التلقائي ، اكتمل SPASS. خلط
قد يؤدي الوضع التلقائي مع الخيارات التي يحددها المستخدم إلى تدمير الاكتمال. الافتراضي هو 1.

-ستدين
لتمكين / تعطيل الإدخال في SPASS عبر stdin. يتم تجاهل وسيطة الملف. الافتراضي هو 0.

-تفاعل
يمكّن / يعطل الوضع التفاعلي. أولاً ، يتم إعطاء SPASS مجموعة من البديهيات ثم
يقبل المُثبِّت مهام الإثبات اللاحقة. الافتراضي هو 0.

-فلوتر
لتمكين / تعطيل وضع ترجمة CNF الخاص بـ SPASS. إذا تم تعيين الخيار ، SPASS فقط
ينفذ بند ترجمة النموذج العادي. إذا لم يتم إعطاء وسيطة ملف الإخراج SPASS
يطبع CNF إلى stdout. الافتراضي هو 0.

-SOS
يمكّن / يعطل مجموعة إستراتيجية الدعم. الافتراضي هو 0.

- انشقاقات =n
يضبط عدد تطبيقات التقسيم الممكنة إلى n. إذا n= -1 ثم عدد
لا يقتصر الانقسامات. الافتراضي هو 0.

-الذاكرة =n
يضبط مقدار الذاكرة المتاحة لـ SPASS لإجراء بحث الإثبات n بايت. ال
الذاكرة المطلوبة لبدء تشغيل SPASS لا يمكن تقييدها. الافتراضي هو -1 يعني ذلك
يتم تقييد عمليات تخصيص الذاكرة فقط بالذاكرة المتوفرة.

-TimeLimit =n
يعيّن حدًا زمنيًا لبحث الإثبات على n ثواني. الافتراضي هو -1 مما يعني أن SPASS
قد يعمل إلى الأبد. يتم استقصاء الحد الزمني عندما يختار SPASS بندًا جديدًا لـ
الاستدلالات. إذا تسببت خطوة استدلال واحدة في حدوث انفجار في عدد العناصر التي تم إنشاؤها
البنود قد يحدث أن يتم تجاوز حد زمني معين بشكل كبير.

-DocSST
لتمكين / تعطيل إخراج الوثائق للكتابة الناعمة الثابتة. نظرية الفرز المستخدمة مثل
وكذلك تتم طباعة محاولة الاختبار (الفاشلة) لقيد الفرز. الافتراضي هو 0.

-دوكبروف
لتمكين / تعطيل إثبات التوثيق. إذا عثر SPASS على إثبات ، فسيتم طباعته في النهاية.
إذا عثرت SPASS على تشبع ، فستتم طباعة مجموعة الجمل المشبعة في النهاية.
قد يؤدي تمكين توثيق الإثبات إلى تقليل أداء SPASS بشكل كبير ، وذلك بسبب
يجب على المُثبِّت تخزين الجمل التي يمكن التخلص منها بطريقة أخرى. الافتراضي هو 0.

-دوكسبليت
يعيّن توثيق خطوات التراجع المنقسم. إذا تم الضبط على 1 ، فإن التيار
تتم طباعة مستوى التراجع. إذا تم ضبطه على 2 ، فإنه يطبع أيضًا في حالة الانقسام
التراجع عن clauese التراجع. الافتراضي هو 0.

- الحلقات
يضبط العدد الأقصى لتكرارات الحلقة الرئيسية لـ SPASS. الافتراضي هو -1.

-PSub
لتمكين / تعطيل طباعة البنود الفرعية. الافتراضي هو 0.

-بريو
لتمكين / تعطيل طباعة تطبيقات إعادة الكتابة البسيطة. الافتراضي هو 0.

-Pon
لتمكين / تعطيل طباعة تطبيقات التكثيف. الافتراضي هو 0.

-بتوت
لتمكين / تعطيل طباعة تطبيقات حذف الحشو. الافتراضي هو 0.

-ببف
تمكين / تعطيل طباعة تطبيقات الاختزال الواضحة. الافتراضي هو 0.

-PSSi
لتمكين / تعطيل طباعة تطبيقات تبسيط الفرز. الافتراضي هو 0.

-PSST
لتمكين / تعطيل طباعة تطبيقات الكتابة الثابتة الثابتة. جميع البنود المحذوفة
طبع. الافتراضي هو 0.

-بمر
لتمكين / تعطيل طباعة تطبيقات دقة الاستبدال المطابقة. الافتراضي هو
0.

-PUnC
لتمكين / تعطيل طباعة تطبيقات تعارض الوحدة. الافتراضي هو 0.

-سعر
لتمكين / تعطيل طباعة الجمل حيث تمت إزالة المعادلات المكررة
(حذف معادلة التخصيص).

-PDer
لتمكين / تعطيل طباعة الجمل المشتقة من الاستدلالات. الافتراضي هو 0.

- نظرا
لتمكين / تعطيل طباعة الجملة المحددة ، المحددة لتنفيذ الاستدلالات.
الافتراضي هو 0.

- ملصقات
لتمكين / تعطيل طباعة الملصقات. إذا تم تعيين -DocProof ولا توجد تسميات لـ
يتم توفير الصيغ من خلال الإدخال ، ينشئ SPASS تسميات عامة يتم توفيرها بعد ذلك
طبع عن طريق تمكين هذا الخيار. الافتراضي هو 0.

-PKept
لتمكين / تعطيل طباعة البنود المحفوظة. هذه هي الجمل التي تم إنشاؤها بواسطة الاستدلالات
(التراجع) التي ليست زائدة عن الحاجة. اشتقت البنود أثناء الإدخال
لا تتم طباعة تقليل / تشبع. الافتراضي هو 0.

-P مشكلة
لتمكين / تعطيل طباعة مجموعة جملة الإدخال. الافتراضي هو 1.

-PmptyClause
لتمكين / تعطيل طباعة العبارات الفارغة المشتقة. الافتراضي هو 0.

إحصائية
تمكين / تعطيل طباعة الإحصائيات النهائية حول البنود المشتقة / المتخلفة / المحفوظة ،
إجراء الانقسامات والوقت المستخدم والمساحة المستخدمة. الافتراضي هو 1.

نموذج
لتمكين / تعطيل إخراج نموذج تم العثور عليه أخيرًا إلى ملف. إذا تم التعيين على 1 ، فكل شيء
تتم طباعة الجمل في المجموعة النهائية. في حالة التعيين على 2 ، فقط البنود التي يمكن أن تكون منتجة
تتم طباعتها ، وهي عبارة عن جمل بدون حرف سالب محدد وقيمة قصوى موجبة
واحد. لو هو اسم مشكلة الإدخال والتي تم إنشاؤها في النهاية
المجموعة مشبعة ، تتم طباعة التشبع على الملف .model ، لـ
خلاف ذلك .شروط. قد تكون الحالة الأخيرة ، على سبيل المثال ، ناجمة عن وقت
حد. الافتراضي هو 0.

-FPDFGProof
لتمكين / تعطيل إخراج إثبات لملف تم العثور عليه أخيرًا. باستخدام هذا الخيار
يتطلب ضبط الخيار -DocProof. لو هو اسم الإدخال
المشكلة تتم طباعة الدليل عليها .prf. الافتراضي هو 0.

-أعلام
لتمكين / تعطيل إخراج جميع قيم العلم. تتم طباعة إعدادات العلم في
نهاية SPASS يتم تشغيلها في شكل قسم إدخال DFG-Syntax. الافتراضي هو 0.

-بتسكوليم
لتمكين / تعطيل إخراج تطبيقات Skolemization المحسنة. الافتراضي هو 0.

-PStrSkolem
لتمكين / تعطيل إخراج تطبيقات Skolemization القوية. الافتراضي هو 0.

-PBDC
لتمكين / تعطيل إخراج الجمل المحذوفة بسبب القيود المقيدة. تقصير
هو 0.

-PBInc
لتمكين / تعطيل إخراج تغييرات التقييد المنضم. الافتراضي هو 0.

-ApplyDefs
لتمكين / تعطيل طباعة توسعات تعريفات الذرة. الافتراضي هو 0.

-تحديد
يحدد استراتيجية الاختيار لـ SPASS. إذا تم التعيين على 0 ، فلن يتم تحديد القيم الحرفية السلبية
تم. إذا تم التعيين على أي قيمة أخرى ، فسيكون على الأكثر قيمة سالبة واحدة في الجملة
المحدد. إذا تم التعيين على 1 قيمة حرفية سالبة في الجمل التي تحتوي على أكثر من قيمة حرفية واحدة كحد أقصى
تم اختيارهم. إما حرفية سالبة بمسند من قائمة الاختيار (انظر
أدناه) أو إذا لم يتوفر مثل هذا الحرفي السلبي ، فسيتم اختيار حرفي سالب مع
يتم اختيار الوزن الأقصى. إذا تم التعيين على 2 حرفية سلبية يتم تحديدها دائمًا. مرة أخرى،
إما حرفية سالبة بمسند من قائمة الاختيار (انظر أدناه) هي
تم اختياره أو في حالة عدم توفر مثل هذا المعنى الحرفي السلبي ، يتم اختيار حرفي سالب مع أقصى حد
الوزن المختار. الحالة الأخيرة ينتج عنها حل مفرط مرتب مثل السلوك
من القرار المطلوب. إذا تم تعيينه على 3 ، أي قيمة حرفية سلبية مع المسند المحدد بواسطة
تم تحديد قائمة الاختيار (انظر أدناه). الافتراضي هو 1.

-R الإدخال
لتمكين / تعطيل تقليل مجموعة الجملة الأولية. الافتراضي هو 1.

-الفرق
تحدد القيم الحرفية الأحادية التي أنشأت قيد الفرز للجملة الأولية
تعيين. إذا تم التعيين على 0 ، فلن يتم إنشاء أي قيد للفرز. إذا تم الضبط على 1 ، كل أحادي السالب
القيم الحرفية مع متغير كوسيطة تشكل قيد الفرز. إذا تم الضبط على 2 ، فكل شيء
تشكل القيم الأحادية السالبة قيد الفرز. قد يضر ضبط الأنواع إلى 2
الاكتمال ، لأن قيود الفرز تخضع للاستراتيجية الأساسية والثابتة
الكتابة الناعمة. الافتراضي هو 1.

-SatInput
لتمكين / تعطيل تشبع الإدخال. التشبع غير مكتمل ولكنه مضمون
إنهاء. الافتراضي هو 0.

-نسبة WDR
يضبط النسبة بين العبارات المحددة حسب الوزن أو العمق في البحث
فضاء. الوزن هو مجموع أوزان الرموز المحددة بواسطة -FuncWeight و
-VarWeight خيارات. عمق جميع الجمل الأولية هو 0 والجمل التي تم إنشاؤها بواسطة
تحصل الاستنتاجات على أقصى عمق للجملة الأصلية بالإضافة إلى 1. القيمة الافتراضية هي 5 ، بمعنى
أن 4 جمل يتم تحديدها حسب الوزن ويتم تحديد البند الخامس حسب العمق.

-PrefCon
يضبط النسبة لحساب وزن عبارات التخمين ، وبالتالي يسمح بـ
تفضل هؤلاء. الافتراضي هو 0 مما يعني أن حساب الوزن لعبارات التخمين
لم يتغير.

-أحمر كامل
لتمكين / تعطيل التخفيض الكامل. إذا تم التعيين على 0 ، فستكون مجموعة الجمل التي تم إيقافها فقط هي
تماما بين مختزلة. إذا تم التعيين على 1 ، فإن جميع بنود التعليق حاليًا (تم إيقاف تشغيلها و
قابلة للاستخدام) مختزلة تمامًا. الافتراضي هو 1.

الوزن
يضبط وزن الوظيفة / الرموز الأصلية. وزن البنود هو مجموع الكل
أوزان الرمز. يتم أخذ هذا الوزن في الاعتبار لاختيار البند المحدد.
الافتراضي هو 1.

-فار الوزن
يضبط وزن الرموز المتغيرة (انظر -FuncWeight). الافتراضي هو 1.

-PrefVar
لتمكين / تعطيل تفضيل الجمل ذات المتغيرات المتعددة. بينما الجمل
يتم تحديده حسب الوزن ، إذا تم تعيين هذا الخيار وكان هناك جملتان لهما نفس الأهمية ، فسيتم تحديد
ويفضل شرط مع تكرارات أكثر تنوعًا. الافتراضي هو 0.

-BoundMode
يحدد وضع القيود المقيدة. الوضع 0 يعني عدم وجود قيود ، إذا تم ضبطه على 1 الكل
البنود التي تم إنشاؤها حديثًا مقيدة بالوزن (انظر -BoundStart) وإذا تم ضبطها على 2
الجمل مقيدة بالعمق. الافتراضي هو 0.

-BoundStart
قيد بدء وضع الحد المحدد. على سبيل المثال ، إذا كان الوضع المرتبط هو 1 و
تم ضبط البداية المقيدة على 5 ، يتم حذف جميع الجمل التي يزيد وزنها عن 5 حتى
المجموعة مشبعة. يؤدي هذا إلى زيادة القيمة المرتبطة المستخدمة التي يتم تحديدها
من خلال الحد الأدنى من الزيادة مع حفظ شرط قبل حذفه. الافتراضي هو -1 بمعنى غير ملزم
تقييد.

-منضم الحلقات
عدد الحلقات التي تطبق قيود الإجراءات / زيادة الحد. إذا كان الرقم
تم تجاوز عدد الحلقات ، يتم إلغاء جميع القيود المقيدة. الافتراضي هو 1.

-ApplyDefs
يضبط العدد الأقصى لتطبيقات تعريفات الذرة على معادلات الإدخال.
الافتراضي هو 0 ، مما يعني عدم وجود تطبيقات على الإطلاق.

- الطلب
يعيّن مصطلح الطلب. إذا تم تحديد 0 ثم KBO ، إذا تم تحديد 1 RPOS. تقصير
هو 0.

-CNFQuantExch
في حالة الضبط ، يتم استبدال مصطلحات Skolem غير الثابتة في الشكل الكلبي للتخمين
بالثوابت. سيتم تعيينه تلقائيًا للترجمة الوظيفية المحسنة لـ
صيغ المنطق الشرطي أو الوصف. الافتراضي هو 0.

-CNFOptSkolem
يمكّن / يعطل Skolemization المحسّن. الافتراضي هو 1.

-CNFStrSkolem
لتمكين / تعطيل Skolemization القوية. الافتراضي هو 1.

-خطوات مقاومة CNF
يعيّن الحد الأقصى لعدد خطوات الإثبات في محاولة محسّنة لإثبات Skolemization.
الافتراضي هو 100.

-CNFSub
لتمكين / تعطيل الاشتراك في البنود التي تم إنشاؤها بواسطة إجراء CNF. تقصير
هو 1.

-CNFC
تمكين / تعطيل التكثيف في الجمل التي تم إنشاؤها بواسطة إجراء CNF. الافتراضي هو
1.

-CNFRedTime
يضبط مقدار الوقت الإجمالي بالثواني لإنفاقه على التخفيض أثناء CNF
تحويل. التخفيضات المتأثرة هي تحسين Skolemization والتكثيف و
الاستيعاب. الافتراضي هو -1 مما يعني أن وقت التخفيض غير محدود على الإطلاق.

-CNF إعادة تسمية
لتمكين / تعطيل إعادة تسمية الصيغة. إذا تم التعيين على 1 يتم تمكين إعادة التسمية المحسنة ذلك
يقلل من عدد البنود التي تم إنشاؤها في النهاية. إذا تم التعيين على 2 معقد ، يتم إعادة تسمية
مُمكّن يقدم مسند Skolem جديدًا لكل صيغة معقدة ، أي ، أي
صيغة ليست حرفية. إذا تم التعيين إلى 3 يتم تمكين إعادة تسمية ذلك
يقدم مسند Skolem جديدًا لكل صيغة فرعية بدءًا من المحدد الكمي.
الافتراضي هو 1.

-CNFRenMatch
في حالة الضبط ، يتم استبدال الصيغ الفرعية المتغيرة بإعادة تسمية الصيغة الحرفية نفسها Skolem. تقصير
هو 1.

-CNFP إعادة تسمية
لتمكين / تعطيل طباعة تطبيقات إعادة تسمية الصيغة. الافتراضي هو 0.

-CNFFEqR
تمكين / تعطيل بعض تقنيات تقليل المساواة على مستوى الصيغة. تقصير
هو 1.

-ImS
لتمكين / تعطيل قاعدة الاستدلال الفرز الفارغ. الافتراضي هو 0.

-هو أو
لتمكين / تعطيل قرار فرز قاعدة الاستنتاج. الافتراضي هو 0.

-معادلة
لتمكين / تعطيل قرار المساواة لقاعدة الاستنتاج. الافتراضي هو 0.

-إيير
لتمكين / تعطيل قرار انعكاس قاعدة الاستدلال. الافتراضي هو 0.

- صندوق
تمكين / تعطيل قاعدة الاستدلال عامل المساواة. الافتراضي هو 0.

- IMPm
يمكّن / يعطل قاعدة الاستنتاج دمج Paramodulation. الافتراضي هو 0.

-ISPR
يمكّن / يعطل قاعدة الاستدلال التراكب الصحيح. الافتراضي هو 0.

-IOPm
تمكين / تعطيل Paramodulation المطلوب لقاعدة الاستدلال. الافتراضي هو 0.

- ISPm
لتمكين / تعطيل قاعدة الاستدلال Paramodulation القياسي. الافتراضي هو 0.

-ISpL
لتمكين / تعطيل قاعدة الاستنتاج تراكب اليسار. الافتراضي هو 0.

-IORe
لتمكين / تعطيل القرار المطلوب لقاعدة الاستنتاج. إذا تم التعيين على 1 ، تم طلبه
تم تمكين الدقة ولكن لا يتم إنشاء استنتاجات دقة مع المعادلات. لو
مضبوطة على 2 ، يتم اعتبار المعادلات لخطوات الحل المطلوب أيضًا. الافتراضي هو
0.

- مصر
لتمكين / تعطيل قاعدة الاستدلال Standard Resolution. إذا تم التعيين على 1 ، قياسي
تم تمكين الدقة ولكن لا يتم إنشاء استنتاجات دقة مع المعادلات. لو
مضبوطة على 2 ، تعتبر المعادلات لخطوات الدقة القياسية أيضًا. الافتراضي هو
0.

-أنا خجولة
لتمكين / تعطيل قاعدة الاستدلال Standard Hyper-Resolution. الافتراضي هو 0.

-IOHy
يمكّن / يعطل قاعدة الاستدلال Ordered Hyper-Resolution. الافتراضي هو 0.

-IURR
لتمكين / تعطيل قرار الوحدة الناتج عن قاعدة الاستنتاج. الافتراضي هو 0.

-IOFc
تمكين / تعطيل العوملة المرتبة لقاعدة الاستدلال. إذا تم التعيين على 1 ، فسيتم ترتيب العوملة
تم تمكينه ولكن يتم إنشاء الاستدلالات ذات القيم الحرفية الإيجابية فقط. إذا تم ضبطه
إلى 2 ، يتم اعتبار القيم الحرفية السالبة للاستدلالات أيضًا. الافتراضي هو 0.

-ISFc
تمكين / تعطيل قاعدة الاستدلال العوملة القياسية. الافتراضي هو 0.

-IUnR
لتمكين / تعطيل قرار وحدة قاعدة الاستنتاج. الافتراضي هو 0.

-إيبور
لتمكين / تعطيل قرار وحدة العمق المحدد لقاعدة الاستنتاج. الافتراضي هو 0.

-IDEF
لتمكين / تعطيل قاعدة الاستنتاج تطبيق التعريفات. غير مدعوم حاليًا.
الافتراضي هو 0.

-RFrew
تمكين / تعطيل إعادة الكتابة إلى الأمام لقاعدة التخفيض. إذا تم التعيين على وحدة واحدة لإعادة الكتابة و
تم تنشيط إعادة الكتابة بدون وحدة بناءً على اختبار القبول. إذا تم الضبط على 2 بالإضافة إلى ذلك
إلى وحدة وغير وحدة إعادة الكتابة السياقية المحلية تنشيط. إذا تم الضبط على 3
بالإضافة إلى إعادة كتابة السياق السياقي للوحدة وغير الوحدة هو
تفعيلها. تتضمن إعادة الكتابة السياقية الفرعية إعادة الكتابة السياقية المحلية. إذا تم ضبطه
إلى 4 بالإضافة إلى قواعد إعادة الكتابة المكونة من 3 ، فإن إعادة الكتابة السياقية الفرعية تختبر أيضًا
للحذف الحرفي السلبي. الافتراضي هو 0.

-RBew
تمكين / تعطيل إعادة الكتابة العكسية لقاعدة التخفيض. نفس القيم والمعنى
للعلم -RFRew ولكنها تستخدم في الاتجاه الخلفي. الافتراضي هو 0.

-RFMRR
لتمكين / تعطيل قرار استبدال المطابقة الأمامية لقاعدة التخفيض. تقصير
هو 0.

-RBMRR
تمكين / تعطيل قرار استبدال المطابقة العكسي لقاعدة التخفيض. تقصير
هو 0.

-RObv
تمكين / تعطيل قاعدة التخفيض "التخفيض الواضح". الافتراضي هو 0.

-RUnC
لتمكين / تعطيل تعارض وحدة قاعدة التخفيض. الافتراضي هو 0.

-رتير
لتمكين / تعطيل حرف النهاية عن طريق تعيين الحد الأقصى لعدد الجمل غير المكونة من وحدة إلى
يمكن استخدامها أثناء البحث. الافتراضي هو 0.

-RTaut
لتمكين / تعطيل حذف قاعدة التخفيض. إذا تم التعيين على 1 ، فسيكون فقط نحويًا
تم الكشف عن الحشو وحذفها. إذا تم ضبطه على 2 ، فإن الحشو الدلالي الإضافي
تتم إزالة. الافتراضي هو 0.

-RSST
لتمكين / تعطيل قاعدة التصغير Static Soft Typing. الافتراضي هو 0.

-RSSi
لتمكين / تعطيل قاعدة تبسيط الفرز لقاعدة التخفيض. الافتراضي هو 0.

-RFSub
لتمكين / تعطيل قاعدة التخفيض إلى الأمام حذف الاشتراك. الافتراضي هو 0.

-RBSub
يمكّن / يعطل قاعدة التخفيض حذف الاسترداد العكسي. الافتراضي هو 0.

-ريد
لتمكين / تعطيل حذف معادلة التعيين لقاعدة التخفيض. هذه القاعدة تزيل
تكرارات معينة من المعادلات من الجمل. إذا تم الضبط على 1 ، يكون التخفيض
مضمون أن يكون سليمًا. في حالة الضبط على 2 ، يكون التخفيض سليمًا فقط إذا كان هناك احتمال
نموذج المشكلة المدروسة له مجال غير تافه. الافتراضي هو 0.

-RCon
لتمكين / تعطيل تكثيف قاعدة التخفيض. الافتراضي هو 0.

-TDfg2OtterOtterOtions
لتمكين / تعطيل تضمين رأس خيارات Otter. هذا الخيار ينطبق فقط على
dfg2otter. إذا تم الضبط على 1 ، فإنه يتضمن إعدادًا يجعل Otter شبه مكتمل. إذا تم ضبطه
على 2 ينشط الوضع التلقائي وإذا تم ضبطه على 3 فإنه ينشط وضع auto2. الافتراضي هو
0.

-EML
علامة EML خاصة للمنطق الشرطي أو صيغ منطق الوصف. لا داعي لذلك
صراحة. تم ضبطه أثناء التحليل.

-EML تلقائي
مخصص لوضع EML الذاتي ، ولكنه لا يعمل حتى الآن. الافتراضي هو 0.

-EMLالترجمة
تحدد طريقة الترجمة المستخدمة للمنطق الشرطي أو صيغ منطق الوصف.
إذا تم الضبط على 0 ، فإن طريقة الترجمة العلائقية القياسية (والتي يتم تحديدها بواسطة
دلالات كريبك المعتادة). إذا تم الضبط على 1 ، فإن طريقة الترجمة الوظيفية هي
مستخدم. إذا تم الضبط على 2 ، يتم استخدام طريقة الترجمة الوظيفية المحسنة. إذا تم التعيين على 3 ،
يتم استخدام طريقة الترجمة شبه الوظيفية. تباين من الأمثل
يتم استخدام طريقة الترجمة الوظيفية ، عند تحديد الإعدادات التالية:
-EMLTranslation = 2 -EMLFuncNary = 1. ستكون الترجمة بلغة n-ary
المسندات بدلاً من المسندات والمسارات الأحادية. في التنفيذ الحالي
طريقة الترجمة العلائقية القياسية هي الأكثر عمومية. تنطبق بعض القيود على
أساليب أخرى. طريقة الترجمة الوظيفية والترجمة شبه الوظيفية
الأساليب المتاحة فقط للمنطق الأساسي متعدد الوسائط K(م) ربما مع المسلسل
(إجمالي) الطرائق (-EML Theory = 1) ، بالإضافة إلى الأسماء الاسمية (عبارات ABox) ، والمصطلحات
البديهيات والبديهيات العامة للتضمين والتكافؤ. الوظيفة الأمثل
طرق الترجمة تنفذ فقط من أجل K(م) ، ربما مع الطرائق التسلسلية.
الافتراضي هو 0.

-EML2Rel
في حالة الضبط ، يتم تحويل الصيغ المقترحة / المنطقية إلى صيغ علائقية
قبل أن يتم ترجمتها إلى منطق من الدرجة الأولى. الافتراضي هو 0.

-نظرية EML
يحدد نظرية الخلفية المفترضة. إذا تم الضبط على 0 ، فإن نظرية الخلفية تكون
فارغ. إذا تم الضبط على 1 ، فسيتم إضافة التسلسل (نظرية الخلفية للدينار الكويتي) للجميع
أشكال. إذا تم ضبطه على 2 ، فسيتم إضافة الانعكاسية (نظرية الخلفية لـ KT)
كل الطرائق. إذا تم الضبط على 3 ، فسيتم إضافة التناظر (نظرية الخلفية لـ KB)
لجميع الطرائق. إذا تم الضبط على 4 ، فإن العبور (نظرية الخلفية لـ K4) هو
أضيفت لجميع الطرائق. إذا تم الضبط على 5 ، فإن الإقليدية (نظرية الخلفية لـ
K5) لجميع الطرائق. إذا تم ضبطه على 6 ، ثم الانتقال والإقليدية
تمت إضافة (نظرية الخلفية لـ S4) لجميع الطرائق. إذا تم التعيين على 7 ، فحينئذٍ
تمت إضافة الانعكاسية والعبودية والإقليدية (نظرية الخلفية لـ S5)
لجميع الطرائق. الافتراضي هو 0.

-EMLFuncNdeQ
في حالة التعيين ، تتم ترجمة الصيغ الماسية وفقًا لـ tr (dia (phi)، s) = nde (s) / \ موجود
x tr (phi، [sx]) (صيغة nde / quantifier) ​​، وإلا فستكون الترجمة بتنسيق
بالتوافق مع tr (dia (phi)، s) = موجود x nde (s) / \ tr (phi، [sx]) (محدد كمي / nde
معادلة). يتم تحديد ترجمة صيغ الصندوق بشكل مزدوج. تحديد هذا العلم هو
يكون ذا مغزى فقط عندما يكون علم طريقة الترجمة الوظيفية أو شبه الوظيفية
تم تعيينه. الافتراضي هو 1.

-EMLFuncNary
في حالة الضبط ، يتم استخدام الترجمة الوظيفية إلى المنطق المخدد. هذا يعني n-ary
يتم استخدام رموز المسند بدلاً من رموز ومسارات المسند الأحادي. تحديد هذا
العلم ذو معنى فقط لاختبار الرضا / الصلاحية المحلي في K متعدد الوسائط.
الافتراضي هو 0.

-EMLFFSorts
في حالة التعيين ، يتم استخدام أنواع المصطلحات. الافتراضي هو 0.

-EMLElimComp
إذا تم ضبطه ، فحاول استبعاد التركيب العلائقي في المعلمات الشرطية. الافتراضي هو 0.

-EMLPTrans
في حالة الضبط ، يتم توثيق EML للترجمة المنطقية من الدرجة الأولى. الافتراضي هو 0.

-تبت
في حالة الضبط ، يتوقع SPASS وجود ملف إدخال في بناء جملة TPTP. الافتراضي هو 0.

-rf في حالة الضبط ، يحذف SPASS ملف الإدخال قبل الإنهاء. الافتراضي هو 0.

أمثلة

لتشغيل SPASS على ملف واحد بدون خيارات:

SPASS الأول

لتعطيل كافة مخرجات SPASS باستثناء النتيجة النهائية:

SPASS - يعطى = 0 - مشكلة P = 0 I

الملاحظات

يمكنك أيضًا تحديد خيارات SPASS في مشكلة الإدخال. في صيغة DFG ، ستفعل
تستخدم

list_of_settings (SPASS).
{*
set_flag (DocProof، 1).
*}
end_of_list.

لتعيين علامة DocProof.

هناك ثلاثة أنواع من الخيارات التي يمكنك تعيينها في الإدخال:

set_flag ( و ).
يضبط العلم على قيمة. تم وصف العلامات والقيم الصالحة في قسم OPTIONS.

تعيين_أسبقية ( ).
يضبط أسبقية الرموز المدرجة. الأسبقية تتناقص من اليسار إلى
يمينًا ، أي أن الرمز الموجود في أقصى اليسار له الأسبقية الأعلى.

كل إدخال في القائمة لديه الشكل

رمز | (SYMBOL، WEIGHT [، {l، r، m}])

يمكنك استخدام النموذج الثاني لتعيين أوزان للرموز (لـ KBO) أو الحالة (لـ
RPOS). الحالة هي إماt {l} من اليسار إلى اليمين ، أوt {m} للمجموعة المتعددة ، أوt {r} لـ
من اليمين الى اليسار. يتم إعطاء الوزن كعدد صحيح.

set_DomPred ( ).
المسند المدرجة (دومبريد للمسند السائد) يتم ترتيب الرموز أولاً وفقًا
على أسبقيتهم ، وليس حسب قوائم الحجج الخاصة بهم. فقط في حالة المساواة
المسندات ، يتم فحص الحجج. على سبيل المثال ، إذا أضفنا الخيار

set_DomPred (P).

ثم في الفقرة

-> R (f (x، y)، a)، P (x، a).

الذرة ف (س ، أ) هو الحد الأقصى بدقة. المسندات المدرجة من قبل set_DomPred الخيار
مقارنة بالأسبقية.

set_selection ( ).
يضبط قائمة الاختيار التي يمكن استخدامها بواسطة علامة التحديد (انظر أعلاه).

set_ClauseFormulaRelation ( ، تسلسل
سلاسل اسم البديهية)).
تم تعيين هذه القائمة بشكل خاص بواسطة FLOTTER وتمكن SPASS من العثور عليها في النهاية
إثبات لإظهار العلاقة بين الجمل المستخدمة في الإثبات والمدخلات
الصيغ. إذا تم دمجها مع خيار DocProof ، فيجب أن يكون هناك إدخال لكل ملف
رقم البند. وإلا تم الإبلاغ عن خطأ.

set_ClauseFormulaRelation((1,ax2),(2,ax1),(3,ax3,ax1)).

استخدم FLOTTER عبر الإنترنت باستخدام خدمات onworks.net