2025-11-23T13:43:17.173951

Admissibility of Substitution Rule in Cyclic-Proof Systems

Saotome, Nakazawa
This paper investigates the admissibility of the substitution rule in cyclic-proof systems. The substitution rule complicates theoretical case analysis and increases computational cost in proof search since every sequent can be a conclusion of an instance of the substitution rule; hence, admissibility is desirable on both fronts. While admissibility is often shown by local proof transformations in non-cyclic systems, such transformations may disrupt cyclic structure and do not readily apply. Prior remarks suggested that the substitution rule is likely nonadmissible in the cyclic-proof system CLKID^omega for first-order logic with inductive predicates. In this paper, we prove admissibility in CLKID^omega, assuming the presence of the cut rule. Our approach unfolds a cyclic proof into an infinitary form, lifts the substitution rules, and places back edges to construct a cyclic proof without the substitution rule. If we restrict substitutions to exclude function symbols, the result extends to a broader class of systems, including cut-free CLKID^omega and cyclic-proof systems for the separation logic.
academic

قابلية قبول قاعدة الاستبدال في أنظمة الإثبات الدورية

المعلومات الأساسية

  • معرّف الورقة: 2510.14749
  • العنوان: قابلية قبول قاعدة الاستبدال في أنظمة الإثبات الدورية
  • المؤلفون: كينجي ساوتومي، كوجي ناكازاوا (جامعة ناغويا)
  • التصنيف: cs.LO (المنطق)
  • تاريخ النشر: 16 أكتوبر 2025
  • رابط الورقة: https://arxiv.org/abs/2510.14749

الملخص

تبحث هذه الورقة مسألة قابلية قبول قاعدة الاستبدال في أنظمة الإثبات الدورية. تعقّد قاعدة الاستبدال التحليل النظري وتزيد من التكلفة الحسابية لبحث الإثبات، لأن كل متتالية قد تكون نتيجة لمثيل من قاعدة الاستبدال، لذا فإن قابلية القبول مرغوبة من الناحية النظرية والعملية على حد سواء. بينما يتم إثبات قابلية القبول عادة من خلال تحويلات الإثبات المحلية في الأنظمة غير الدورية، قد تؤدي هذه التحويلات إلى تدمير البنية الدورية ولا يمكن تطبيقها مباشرة. أظهرت الأبحاث السابقة أن قاعدة الاستبدال في نظام الإثبات الدوري من الدرجة الأولى CLKIDω مع المسندات الاستقرائية من المحتمل أن تكون غير قابلة للقبول. تثبت هذه الورقة أنه في وجود قاعدة القطع، قاعدة الاستبدال في CLKIDω قابلة للقبول. يتمثل نهجنا في فك الأثبات الدورية إلى أشكال لا نهائية، ورفع قاعدة الاستبدال، ثم إعادة الحواف لبناء إثبات دوري بدون قاعدة الاستبدال. إذا قيدنا الاستبدال بعدم إدخال رموز دالة، يمكن توسيع هذه النتيجة إلى فئة أوسع من الأنظمة، بما في ذلك CLKIDω بدون قطع وأنظمة الإثبات الدورية للمنطق الفاصل.

الخلفية البحثية والدافع

تعريف المشكلة

الأثبات الدورية هي امتداد لأشجار الإثبات التقليدية، حيث تقدم بنى دورية للاستدلال حول المسندات المعرّفة بشكل استقرائي. تُدخل قاعدة الاستبدال Γ⊢ΔΓ[θ]⊢Δ[θ]\frac{\Gamma \vdash \Delta}{\Gamma[\theta] \vdash \Delta[\theta]} (Subst) في العديد من أنظمة الإثبات الدورية لمساعدة بناء البنى الدورية.

أهمية المشكلة

  1. من الناحية النظرية: قاعدة الاستبدال قابلة للتطبيق دائماً، مما يعقّد تحليل الإثبات
  2. من الناحية العملية: التطبيق غير المقيد لقاعدة الاستبدال يزيد من التكلفة الحسابية، لأن العديد من الاستبدالات يمكن تطبيقها في كل خطوة

حدود الطرق الموجودة

في أنظمة الإثبات غير الدورية، عادة ما يتم إثبات قابلية قبول قاعدة الاستبدال من خلال مرحلتين:

  1. مرحلة الرفع: تحريك قاعدة الاستبدال لأعلى
  2. مرحلة الحذف: حذف قاعدة الاستبدال عند البديهيات

لكن في أنظمة الإثبات الدورية، تواجه هذه الطريقة صعوبات أساسية:

  • قد تؤدي مرحلة الرفع إلى تدمير علاقة البرعم والرفيق (bud-companion relationship)
  • لا يمكن حذف الاستبدال عند البراعم في مرحلة الحذف

الدافع البحثي

طرح Brotherston 1 السؤال حول ما إذا كانت قاعدة الاستبدال قابلة للقبول في CLKIDω، مما يشير إلى أنه في الحالة العامة، على الأقل في الإعداد بدون قطع، من المحتمل أن تكون غير قابلة للقبول. تهدف هذه الورقة إلى حل هذه المسألة المفتوحة.

المساهمات الأساسية

  1. النتيجة النظرية الرئيسية: إثبات أنه في وجود قاعدة القطع، قاعدة الاستبدال في CLKIDω قابلة للقبول
  2. النتائج الموسعة: عند تقييد الاستبدال بالاستبدال الذري (عدم إدخال رموز دالة موجبة الأرية)، تتوسع النتيجة إلى CLKIDω بدون قطع
  3. تعميم التطبيق: تنطبق النتيجة على أنظمة إثبات أخرى، مثل أنظمة الإثبات الدورية للمنطق الفاصل
  4. طريقة جديدة: اقتراح استراتيجية حذف من ثلاث خطوات من خلال الفك اللانهائي ورفع الاستبدال وإعادة البناء الدوري

شرح الطريقة

تعريف المهمة

بالنظر إلى إثبات Pr+ في CLKIDω يحتوي على قاعدة الاستبدال، بناء إثبات Pr- لا يحتوي على قاعدة الاستبدال، بحيث يثبت كلاهما نفس المتتالية.

البنية الأساسية للطريقة

تنقسم عملية الحذف في هذه الورقة إلى مرحلتين رئيسيتين:

1. حذف الاستبدالات المركبة

التعريف:

  • الاستبدال الذري: استبدالات تحتوي فقط على متغيرات وثوابت
  • الاستبدال المركب: استبدالات تحتوي على رموز دالة موجبة الأرية

الطريقة: حذف الاستبدالات المركبة من خلال التحويل التالي:

Γ ⊢ Δ
────────────────────────── (Subst)
Γ[x₁:=t₁,...,xₙ:=tₙ] ⊢ Δ[x₁:=t₁,...,xₙ:=tₙ]

تحويل إلى مزيج من قاعدة القطع وقواعد المساواة وقواعس الكم الوجودي، مع الحفاظ في النهاية على الاستبدالات الذرية فقط.

2. حذف الاستبدالات الذرية

هذا هو الابتكار الأساسي، ويتضمن ثلاث خطوات:

الخطوة 1: الفك الدوري

  • فك الإثبات الدوري Pr_var+ إلى إثبات لا نهائي Pr^ω
  • تعريف الخريطة f^ω: Seq(Pr^ω) → Seq(Pr_var+) لربط ظهور المتتاليات

الخطوة 2: رفع الاستبدال

  • بناء إثبات LKIDω بشكل تكراري Pr^ω_d بدون قاعدة الاستبدال ضمن العمق d
  • استخدام خاصية تطبيق الاستبدال (substitution-application property)

الخطوة 3: إعادة البناء الدوري

  • بناء ما قبل إثبات CLKIDω Pr- من Pr^ω_d
  • اختيار البراعم والرفقاء، مع ضمان شرط المسار العام

نقاط الابتكار التقني

1. الإغلاق الاستبدالي الجزئي (Partial-substitution Closure)

التعريف 10: بالنظر إلى مجموعة الاستبدالات Θ ومجموعة المتغيرات X، الإغلاق الاستبدالي الجزئي Cps(Θ,X) هو أصغر مجموعة تحقق:

  • Θ ⊆ Cps(Θ,X)
  • لأي θ∈Cps(Θ,X) و x,y∈X: θx→y ∈ Cps(Θ,X)
  • لأي θ₁,θ₂∈Cps(Θ,X): θ₁θ₂ ∈ Cps(Θ,X)

الخاصية الرئيسية: عند التقييد بالاستبدالات الذرية، يكون الإغلاق الاستبدالي الجزئي محدوداً.

2. خاصية تطبيق الاستبدال (Substitution-application Property)

التعريف 11: تحقق القاعدة (R) خاصية تطبيق الاستبدال، إذا كان لأي مثيل قاعدة واستبدال ذري θ، يوجد مثيل تطبيق استبدال مقابل، مع الحفاظ على المسار.

اللمة 4: CLKIDω و LKIDω يحققان خاصية تطبيق الاستبدال.

3. الحفاظ على شرط المسار العام

ضمان أن الإثبات المعاد بناؤه يحقق شرط المسار العام من خلال مفهوم المسارات المقابلة:

التعريف 12: لمسار (eᵢ) في Pr-، عرّف المسار المقابل (e'ⱼ) في Pr_var+، بحيث يتم الحفاظ على كل مسار لا نهائي متقدم.

الإعداد التجريبي

هذه الورقة عمل نظري بحت، بدون تجارب بالمعنى التقليدي. يتم التحقق من خلال:

التحقق النظري

  1. الإثبات البنائي: إثبات قابلية القبول من خلال بناء خوارزمية صريحة
  2. تحليل الحالات المضادة: تحليل الحالات التي لا تحقق قابلية القبول تحت القيود
  3. توسيع النظام: التحقق من تطبيق النتائج في أنظمة أخرى

تحليل الأمثلة

توفر الورقة أمثلة محددة لتحويل الإثبات:

  • الشكل 1: إثبات دوري يحتوي على قاعدة الاستبدال
  • الشكل 3: الإثبات اللانهائي بعد الفك
  • عرض كيفية حذف قاعدة الاستبدال من الإثبات الدوري لـ N(x) ⊢ E(x)∨O(x)

نتائج التجارب

النتائج النظرية الرئيسية

النظرية 2 (قابلية قبول قاعدة الاستبدال في CLKIDω): إذا كانت Γ ⊢ Δ قابلة للإثبات في CLKIDω، فإنها قابلة للإثبات أيضاً في CLKIDω بدون (Subst).

النظرية 3 (النتيجة القوية للاستبدال الذري): إذا كان Pr إثباتاً لـ Γ ⊢ Δ في CLKIDω و Θ(Pr) يحتوي فقط على استبدالات ذرية، فإنه يوجد إثبات بدون (Subst) يحتوي فقط على القواعد الموجودة في Pr.

النتائج الموسعة

النظرية 4 (قابلية القبول في الأنظمة بدون قطع): في CLKIDω^- (CLKIDω بدون قطع)، قاعدة الاستبدال الذري قابلة للقبول.

النظرية 5 (التطبيق في المنطق الفاصل): قاعدة الاستبدال قابلة للقبول في كل من CSLω و CSLω^-.

النتائج النظرية

  1. الدور الحاسم لقاعدة القطع: حذف الاستبدالات المركبة يتطلب قاعدة القطع
  2. عمومية الاستبدال الذري: حذف الاستبدالات الذرية ينطبق على فئة أوسع من الأنظمة
  3. قيود رموز الدالة: وجود رموز الدالة هو العائق الرئيسي لقابلية القبول

الأعمال ذات الصلة

الاتجاهات البحثية الرئيسية

  1. نظرية الإثبات الدوري: الأعمال الرائدة لـ Brotherston وآخرين 1,4,6
  2. بحث الإثبات: البحث عن تجنب بحث الفرضيات الاستقرائية الاستكشافية 2,3,5,11,12
  3. المنطق الفاصل: تطبيقات الإثبات الدوري في المنطق الفاصل 2,7,9

علاقة هذه الورقة بالأعمال ذات الصلة

  • حل المسألة المفتوحة التي طرحها Brotherston 1
  • توسيع عمل Kimura وآخرين 7 إلى إعدادات أكثر عمومية
  • توفير أساس نظري لبحث الإثبات

مزايا هذه الورقة

  1. الإثبات الأول: أول إثبات صارم لقابلية قبول قاعدة الاستبدال في CLKIDω
  2. ابتكار الطريقة: اقتراح تقنيات حذف جديدة تنطبق على البنى الدورية
  3. التطبيق الواسع: النتائج تنطبق على عدة أنظمة ذات صلة

الخلاصة والنقاش

الاستنتاجات الرئيسية

  1. في وجود قاعدة القطع في CLKIDω، قاعدة الاستبدال قابلة للقبول
  2. عند التقييد بالاستبدالات الذرية، تتوسع النتيجة إلى الأنظمة بدون قطع
  3. تنطبق النتيجة على أنظمة أخرى مهمة مثل المنطق الفاصل

القيود

  1. الاعتماد على قاعدة القطع: حذف الاستبدالات المركبة يتطلب قاعدة القطع
  2. قيود رموز الدالة: النتيجة العامة الكاملة تتطلب استبعاد رموز الدالة
  3. تعقيد البناء: عملية بناء الإثبات معقدة نسبياً

الاتجاهات المستقبلية

  1. مجموعة القواعد الدنيا: البحث عن أصغر مجموعة قواعد تسمح بحذف قاعدة الاستبدال في وجود رموز الدالة
  2. حذف القطع: دراسة خاصية حذف القطع لأنظمة الإثبات الدورية من خلال إدخال قواعد إضافية
  3. التعقيد الحسابي: تحليل التعقيد الحسابي لحذف قاعدة الاستبدال

التقييم المتعمق

المزايا

  1. الأهمية النظرية: حل مسألة مفتوحة مهمة في هذا المجال
  2. ابتكار الطريقة: اقتراح تقنيات جديدة تنطبق على البنى الدورية
  3. الصرامة: الإثبات صارم وبنائي
  4. التطبيق الواسع: النتائج تنطبق على عدة أنظمة ذات صلة
  5. الوضوح: التفاصيل التقنية معروضة بوضوح وسهلة الفهم

أوجه القصور

  1. قيود الفائدة العملية: الاعتماد على قاعدة القطع يحد من التطبيقات العملية
  2. التعقيد: عملية تحويل الإثبات معقدة نسبياً
  3. عدم الاكتمال: في الإعداد بدون قطع لا تزال هناك قيود

التأثير

  1. المساهمة النظرية: توفير أساس نظري مهم لنظرية الإثبات الدوري
  2. القيمة العملية: توفير مرونة أكبر لتطبيقات بحث الإثبات
  3. القابلية للتوسع: قد تنطبق الطريقة على أنظمة أخرى ذات صلة

حالات التطبيق

  1. الإثبات الآلي للنظريات: تحسين كفاءة بحث الإثبات الدوري
  2. التحقق من البرامج: التطبيق في أطر التحقق مثل المنطق الفاصل
  3. البحث النظري: توفير أساس لمزيد من البحث في نظرية الإثبات الدوري

المراجع

تستشهد الورقة بـ 19 مرجعاً ذا صلة، تشمل بشكل أساسي:

  1. الأعمال الرائدة لـ Brotherston في الإثبات الدوري
  2. أبحاث تطبيق الإثبات الدوري في المنطق الفاصل
  3. الأعمال ذات الصلة ببحث الإثبات الآلي
  4. البحث الأساسي في حذف القطع ونظرية الإثبات

تقدم هذه الورقة مساهمة مهمة في نظرية الإثبات الدوري، حيث تحل مسألة مفتوحة مهمة من خلال تقنيات مبتكرة، مما يضع أساساً لمزيد من التطور في هذا المجال.