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 (যুক্তিবিদ্যা)
প্রকাশনার সময়: ২০২৫ সালের ১৬ অক্টোবর
পত্র লিঙ্ক: https://arxiv.org/abs/2510.14749

সারসংক্ষেপ

এই পত্রটি চক্রীয় প্রমাণ ব্যবস্থায় প্রতিস্থাপন নিয়মের গ্রহণযোগ্যতা সমস্যা নিয়ে গবেষণা করে। প্রতিস্থাপন নিয়ম তাত্ত্বিক বিশ্লেষণকে জটিল করে এবং প্রমাণ অনুসন্ধানের গণনামূলক খরচ বৃদ্ধি করে, কারণ প্রতিটি ক্রমাগত প্রতিস্থাপন নিয়মের উদাহরণের সিদ্ধান্ত হতে পারে, তাই গ্রহণযোগ্যতা তাত্ত্বিক এবং ব্যবহারিক উভয় দিক থেকেই আদর্শ। যদিও অ-চক্রীয় ব্যবস্থায় গ্রহণযোগ্যতা সাধারণত স্থানীয় প্রমাণ রূপান্তরের মাধ্যমে প্রমাণিত হয়, এই ধরনের রূপান্তর চক্রীয় কাঠামো ভেঙে ফেলতে পারে এবং সরাসরি প্রয়োগ করা যায় না। পূর্ববর্তী গবেষণা দেখিয়েছে যে প্রতিস্থাপন নিয়ম আনুষঙ্গিক বিধেয় সহ প্রথম-ক্রম যুক্তি চক্রীয় প্রমাণ ব্যবস্থা CLKIDω-তে সম্ভবত অগ্রহণযোগ্য। এই পত্রটি প্রমাণ করে যে কাটা নিয়মের উপস্থিতিতে, CLKIDω-তে প্রতিস্থাপন নিয়ম গ্রহণযোগ্য। আমাদের পদ্ধতি হল চক্রীয় প্রমাণকে অসীম রূপে প্রসারিত করা, প্রতিস্থাপন নিয়ম উন্নীত করা, এবং তারপর প্রান্ত ফিরিয়ে আনা প্রতিস্থাপন নিয়ম ছাড়াই চক্রীয় প্রমাণ তৈরি করতে। যদি প্রতিস্থাপন ফাংশন প্রতীক প্রবর্তন না করার জন্য সীমাবদ্ধ হয়, এই ফলাফল আরও বিস্তৃত ব্যবস্থার বিভাগে প্রসারিত হতে পারে, যার মধ্যে রয়েছে কাটা-মুক্ত CLKIDω এবং বিচ্ছিন্ন যুক্তির চক্রীয় প্রমাণ ব্যবস্থা।

গবেষণা পটভূমি এবং প্রেরণা

সমস্যার সংজ্ঞা

চক্রীয় প্রমাণ হল ঐতিহ্যবাহী প্রমাণ গাছের সম্প্রসারণ, যা চক্রীয় কাঠামো প্রবর্তনের মাধ্যমে আনুষঙ্গিক সংজ্ঞায়িত বিধেয় সম্পর্কে যুক্তি প্রদান করে। প্রতিস্থাপন নিয়ম $\frac{\Gamma \vdash \Delta}{\Gamma[\theta] \vdash \Delta[\theta]}$ (Subst) অনেক চক্রীয় প্রমাণ ব্যবস্থায় প্রবর্তিত হয়েছে, চক্রীয় কাঠামো তৈরিতে সহায়তা করার জন্য।

সমস্যার গুরুত্ব

তাত্ত্বিক দিক: প্রতিস্থাপন নিয়ম সর্বদা প্রয়োগযোগ্য, যা প্রমাণ বিশ্লেষণকে জটিল করে তোলে
ব্যবহারিক দিক: সীমাহীন প্রতিস্থাপন নিয়ম প্রয়োগ গণনামূলক খরচ বৃদ্ধি করে, কারণ প্রতিটি পদক্ষেপে অনেক প্রতিস্থাপন প্রয়োগ করা যেতে পারে

বিদ্যমান পদ্ধতির সীমাবদ্ধতা

অ-চক্রীয় প্রমাণ ব্যবস্থায়, প্রতিস্থাপন নিয়মের গ্রহণযোগ্যতা সাধারণত দুটি পর্যায়ে অর্জিত হয়:

উন্নয়ন পর্যায়: প্রতিস্থাপন নিয়ম উপরের দিকে সরানো
নির্মূলন পর্যায়: স্বতঃসিদ্ধ স্থানে প্রতিস্থাপন নির্মূল করা

কিন্তু চক্রীয় প্রমাণ ব্যবস্থায়, এই পদ্ধতি মৌলিক অসুবিধার সম্মুখীন হয়:

উন্নয়ন পর্যায় কুঁড়ি-সঙ্গী সম্পর্ক (bud-companion relationship) ভেঙে ফেলতে পারে
নির্মূলন পর্যায় কুঁড়িতে প্রতিস্থাপন নির্মূল করতে পারে না

গবেষণা প্রেরণা

ব্রাদারস্টন 1 CLKIDω-তে প্রতিস্থাপন নিয়ম গ্রহণযোগ্য কিনা তা প্রশ্ন করেছেন, যা ইঙ্গিত করে যে সাধারণ ক্ষেত্রে, অন্তত কাটা-মুক্ত সেটিংয়ে, এটি সম্ভবত অগ্রহণযোগ্য। এই পত্রটি এই খোলা সমস্যা সমাধানের লক্ষ্য রাখে।

মূল অবদান

প্রধান তাত্ত্বিক ফলাফল: কাটা নিয়মের উপস্থিতিতে CLKIDω-তে প্রতিস্থাপন নিয়ম গ্রহণযোগ্য প্রমাণ করা
সম্প্রসারণ ফলাফল: যখন প্রতিস্থাপন পরমাণু প্রতিস্থাপনে সীমাবদ্ধ (ইতিবাচক আর্যতা ফাংশন প্রতীক প্রবর্তন না করে), ফলাফল কাটা-মুক্ত CLKIDω-তে প্রসারিত হয়
প্রয়োগ সাধারণীকরণ: এই ফলাফল অন্যান্য প্রমাণ ব্যবস্থায় প্রয়োগযোগ্য, যেমন বিচ্ছিন্ন যুক্তির চক্রীয় প্রমাণ ব্যবস্থা
উদ্ভাবনী পদ্ধতি: অসীম সম্প্রসারণ, প্রতিস্থাপন উন্নয়ন এবং চক্রীয় পুনর্নির্মাণের মাধ্যমে একটি তিন-পদক্ষেপ নির্মূলন কৌশল প্রস্তাব করা

পদ্ধতি বিস্তারিত

কাজের সংজ্ঞা

CLKIDω-তে প্রতিস্থাপন নিয়ম সহ একটি প্রমাণ Pr+ দেওয়া, প্রতিস্থাপন নিয়ম ছাড়াই একটি প্রমাণ Pr- তৈরি করুন, যাতে উভয়ই একই ক্রমাগত প্রমাণ করে।

মূল পদ্ধতি স্থাপত্য

এই পত্রের নির্মূলন প্রক্রিয়া দুটি প্রধান পর্যায়ে বিভক্ত:

1. যৌগিক প্রতিস্থাপনের নির্মূলন

সংজ্ঞা:

পরমাণু প্রতিস্থাপন: শুধুমাত্র ভেরিয়েবল এবং ধ্রুবক সহ প্রতিস্থাপন
যৌগিক প্রতিস্থাপন: ইতিবাচক আর্যতা ফাংশন প্রতীক সহ পদ সহ প্রতিস্থাপন

পদ্ধতি: নিম্নলিখিত রূপান্তরের মাধ্যমে যৌগিক প্রতিস্থাপন নির্মূল করা:

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

কাটা নিয়ম, সমতা নিয়ম এবং অস্তিত্ব পরিমাণকারী নিয়মের সমন্বয় ব্যবহার করে রূপান্তরিত করা, চূড়ান্তভাবে শুধুমাত্র পরমাণু প্রতিস্থাপন সংরক্ষণ করা।

2. পরমাণু প্রতিস্থাপনের নির্মূলন

এটি মূল উদ্ভাবন, তিনটি পদক্ষেপ অন্তর্ভুক্ত:

পদক্ষেপ 1: চক্রীয় সম্প্রসারণ

চক্রীয় প্রমাণ Pr_var+ কে অসীম প্রমাণ Pr^ω-তে প্রসারিত করা
ম্যাপিং f^ω: Seq(Pr^ω) → Seq(Pr_var+) সংজ্ঞায়িত করা যা ক্রমাগত ঘটনা সম্পর্কিত করে

পদক্ষেপ 2: প্রতিস্থাপন উন্নয়ন

গভীরতা d-এর মধ্যে প্রতিস্থাপন নিয়ম ছাড়াই LKIDω প্রমাণ Pr^ω_d পুনরাবৃত্তিমূলকভাবে তৈরি করা
প্রতিস্থাপন প্রয়োগ বৈশিষ্ট্য ব্যবহার করা

পদক্ষেপ 3: চক্রীয় পুনর্নির্মাণ

Pr^ω_d থেকে CLKIDω প্রাক-প্রমাণ Pr- তৈরি করা
কুঁড়ি এবং সঙ্গী নির্বাচন করা, বৈশ্বিক ট্র্যাক শর্ত নিশ্চিত করা

প্রযুক্তিগত উদ্ভাবন পয়েন্ট

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: Pr- এ একটি পথ (eᵢ) এর জন্য, Pr_var+ এ সংশ্লিষ্ট পথ (e'ⱼ) সংজ্ঞায়িত করা, যাতে প্রতিটি অসীম অগ্রগামী ট্র্যাক সংরক্ষিত হয়।

পরীক্ষামূলক সেটআপ

এই পত্রটি বিশুদ্ধ তাত্ত্বিক কাজ, ঐতিহ্যবাহী অর্থে কোনো পরীক্ষা নেই। যাচাইকরণ নিম্নলিখিত উপায়ে পরিচালিত হয়:

তাত্ত্বিক যাচাইকরণ

গঠনমূলক প্রমাণ: স্পষ্ট অ্যালগরিদম নির্মাণের মাধ্যমে গ্রহণযোগ্যতা প্রমাণ করা
প্রতিউদাহরণ বিশ্লেষণ: সীমাবদ্ধ শর্তে গ্রহণযোগ্যতা সন্তুষ্ট না করে এমন ক্ষেত্রে বিশ্লেষণ করা
ব্যবস্থা সম্প্রসারণ: অন্যান্য ব্যবস্থায় ফলাফলের প্রয়োগযোগ্যতা যাচাই করা

উদাহরণ বিশ্লেষণ

পত্রটি নির্দিষ্ট প্রমাণ রূপান্তর উদাহরণ প্রদান করে:

চিত্র 1: প্রতিস্থাপন নিয়ম সহ চক্রীয় প্রমাণ
চিত্র 3: সম্প্রসারণের পরে অসীম প্রমাণ
N(x) ⊢ E(x)∨O(x) এর চক্রীয় প্রমাণ থেকে প্রতিস্থাপন নিয়ম কীভাবে নির্মূল করতে হয় তা প্রদর্শন করা

পরীক্ষামূলক ফলাফল

প্রধান তাত্ত্বিক ফলাফল

উপপাদ্য 2 (CLKIDω-তে প্রতিস্থাপন নিয়মের গ্রহণযোগ্যতা): যদি Γ ⊢ Δ CLKIDω-তে প্রমাণযোগ্য হয়, তাহলে এটি (Subst) ছাড়াই CLKIDω-তে প্রমাণযোগ্য।

উপপাদ্য 3 (পরমাণু প্রতিস্থাপনের শক্তিশালী ফলাফল): যদি Pr CLKIDω-তে Γ ⊢ Δ এর প্রমাণ হয় এবং Θ(Pr) শুধুমাত্র পরমাণু প্রতিস্থাপন অন্তর্ভুক্ত করে, তাহলে (Subst) ছাড়াই একটি প্রমাণ বিদ্যমান থাকে এবং শুধুমাত্র Pr-তে প্রদর্শিত নিয়ম অন্তর্ভুক্ত করে।

সম্প্রসারণ ফলাফল

উপপাদ্য 4 (কাটা-মুক্ত ব্যবস্থায় গ্রহণযোগ্যতা): CLKIDω^- (কাটা-মুক্ত CLKIDω)-তে, পরমাণু প্রতিস্থাপন নিয়ম গ্রহণযোগ্য।

উপপাদ্য 5 (বিচ্ছিন্ন যুক্তিতে প্রয়োগ): প্রতিস্থাপন নিয়ম CSLω এবং CSLω^- উভয়েই গ্রহণযোগ্য।

তাত্ত্বিক আবিষ্কার

কাটা নিয়মের মূল ভূমিকা: যৌগিক প্রতিস্থাপনের নির্মূলন কাটা নিয়ম প্রয়োজন
পরমাণু প্রতিস্থাপনের সর্বজনীনতা: পরমাণু প্রতিস্থাপনের নির্মূলন আরও বিস্তৃত ব্যবস্থায় প্রয়োগযোগ্য
ফাংশন প্রতীকের সীমাবদ্ধতা: ফাংশন প্রতীকের উপস্থিতি গ্রহণযোগ্যতার মূল বাধা

উপসংহার এবং আলোচনা

প্রধান উপসংহার

কাটা নিয়মের উপস্থিতিতে CLKIDω-তে প্রতিস্থাপন নিয়ম গ্রহণযোগ্য
পরমাণু প্রতিস্থাপনে সীমাবদ্ধ হলে, ফলাফল কাটা-মুক্ত ব্যবস্থায় প্রসারিত হয়
এই ফলাফল বিচ্ছিন্ন যুক্তি সহ অন্যান্য গুরুত্বপূর্ণ ব্যবস্থায় প্রয়োগযোগ্য

সীমাবদ্ধতা

কাটা নিয়ম নির্ভরতা: যৌগিক প্রতিস্থাপনের নির্মূলন কাটা নিয়ম প্রয়োজন
ফাংশন প্রতীক সীমাবদ্ধতা: সম্পূর্ণ সাধারণ ফলাফল ফাংশন প্রতীক বাদ দিতে প্রয়োজন
গঠনমূলক জটিলতা: প্রমাণ নির্মাণ প্রক্রিয়া অপেক্ষাকৃত জটিল

ভবিষ্যত দিকনির্দেশনা

ন্যূনতম নিয়ম সেট: ফাংশন প্রতীক উপস্থিত থাকলেও প্রতিস্থাপন নিয়ম নির্মূলের অনুমতি দেয় এমন ন্যূনতম নিয়ম সেট গবেষণা করা
কাটা নির্মূলন: অতিরিক্ত নিয়ম প্রবর্তনের মাধ্যমে চক্রীয় প্রমাণ ব্যবস্থার কাটা নির্মূলন বৈশিষ্ট্য গবেষণা করা
গণনামূলক জটিলতা: প্রতিস্থাপন নিয়ম নির্মূলের গণনামূলক জটিলতা বিশ্লেষণ করা

গভীর মূল্যায়ন

সুবিধা

তাত্ত্বিক গুরুত্ব: এই ক্ষেত্রের একটি গুরুত্বপূর্ণ খোলা সমস্যা সমাধান করা
পদ্ধতি উদ্ভাবন: চক্রীয় কাঠামোর জন্য প্রযোজ্য নতুন কৌশল প্রস্তাব করা
কঠোরতা: প্রমাণ কঠোর এবং গঠনমূলক
ব্যাপক প্রয়োগযোগ্যতা: ফলাফল একাধিক সম্পর্কিত ব্যবস্থায় প্রয়োগযোগ্য
স্পষ্ট উপস্থাপনা: প্রযুক্তিগত বিবরণ স্পষ্টভাবে উপস্থাপিত, বোঝা সহজ

অপূর্ণতা

ব্যবহারিক সীমাবদ্ধতা: কাটা নিয়মের উপর নির্ভরতা ব্যবহারিক প্রয়োগ সীমাবদ্ধ করে
জটিলতা: প্রমাণ রূপান্তর প্রক্রিয়া অপেক্ষাকৃত জটিল
সম্পূর্ণতা: কাটা-মুক্ত সেটিংয়ে এখনও সীমাবদ্ধতা রয়েছে

প্রভাব

তাত্ত্বিক অবদান: চক্রীয় প্রমাণ তত্ত্বের জন্য গুরুত্বপূর্ণ তাত্ত্বিক ভিত্তি প্রদান করা
ব্যবহারিক মূল্য: প্রমাণ অনুসন্ধান বাস্তবায়নে আরও নমনীয়তা প্রদান করা
সম্প্রসারণযোগ্যতা: পদ্ধতি অন্যান্য সম্পর্কিত ব্যবস্থায় প্রয়োগযোগ্য হতে পারে

প্রযোজ্য পরিস্থিতি

স্বয়ংক্রিয় উপপাদ্য প্রমাণ: চক্রীয় প্রমাণ অনুসন্ধানের দক্ষতা উন্নত করা
প্রোগ্রাম যাচাইকরণ: বিচ্ছিন্ন যুক্তি সহ যাচাইকরণ কাঠামোতে প্রয়োগ
তাত্ত্বিক গবেষণা: চক্রীয় প্রমাণ তত্ত্বের আরও গবেষণার জন্য ভিত্তি প্রদান করা

তথ্যসূত্র

পত্রটি 19টি সম্পর্কিত তথ্যসূত্র উদ্ধৃত করে, প্রধানত অন্তর্ভুক্ত:

ব্রাদারস্টনের চক্রীয় প্রমাণ অগ্রগামী কাজ
বিচ্ছিন্ন যুক্তিতে চক্রীয় প্রমাণের প্রয়োগ গবেষণা
স্বয়ংক্রিয় প্রমাণ অনুসন্ধানের সম্পর্কিত কাজ
কাটা নির্মূলন এবং প্রমাণ তত্ত্বের মৌলিক গবেষণা

এই পত্রটি চক্রীয় প্রমাণ তত্ত্বে গুরুত্বপূর্ণ অবদান রাখে, উদ্ভাবনী প্রযুক্তিগত হাতিয়ার ব্যবহার করে একটি গুরুত্বপূর্ণ খোলা সমস্যা সমাধান করে, এই ক্ষেত্রের আরও উন্নয়নের জন্য ভিত্তি স্থাপন করে।