حساب التفاضل والتكامل للهياكل

📅 آخر تحديث: ٢٧ يوليو ٢٠٢٦
✍️ نُشر في: ٢٧ يوليو ٢٠٢٦
📷 يحتوي على 82 صور
الموسوعة الحرة

في المنطق الرياضي ، يُعدّ حساب البنى (CoS) حسابًا للبرهان يتميز بالاستدلال العميق لدراسة نظرية البرهان البنيوية للمنطق غير التبادلي . وقد طُبّق هذا الحساب لاحقًا لدراسة المنطق الخطي ، والمنطق الكلاسيكي ، والمنطق الموجه ، وحساب العمليات ، ويُزعم أن فوائد جمّة تترتب على هذه الدراسات بفضل إمكانية الاستدلال العميق التي يوفرها.

تم تقديمه لأول مرة في عام 2001 في ورقة بحثية بعنوان "نظام التفاعل والبنية" من تأليف أليسيو غولييلمو من جامعة باث . [ 1 ] [ 2 ]

التعريفات

الصيغة هي سلسلة ( سليمة التكوين ) من الرموز المنطقية. على سبيل المثال ،((أ∧ب)∧¬ج)∨د{\displaystyle ((a\land b)\land \neg c)\lor d}هي صيغة.

النظرية المعادلاتية هي قائمة من المعادلات التي تصف علاقة تكافؤ على مجموعة جميع الصيغ. ومن المعادلات الشائعة: معادلات التجميع، ومعادلات التبديل، ومعادلات الثوابت المنطقية.

البنية هي فئة تكافؤ من الصيغ. ويؤكد اسم "البنية" أن CoS لا يميز بين المتتاليات والصيغ، بل يستخدم كائنًا واحدًا للقيام بوظيفة كليهما في حساب المتتاليات. وبشكل أدق، يمكن اعتبار البنية فئة تكافؤ من الصيغ .

السياق هو بنية تم حذف بنية فرعية منها. على سبيل المثال ،أ∧-{\displaystyle A\land -}هو سياق، حيث-{\displaystyle -}يشير إلى بنية فرعية محذوفة. تُكتب السياقات على النحو التالي:S{-}{\displaystyle S\{-\}}فعلى سبيل المثال، إذاS{-}:=أ∧-{\displaystyle S\{-\}:=A\land -}، ثمS{ب}{\displaystyle S\{B\}}يُعرَّف بأنهأ∧ب{\displaystyle A\land B}.

تكون قاعدة الاستدلال على الشكل التالي:S{أ}S{ب}{\displaystyle {\frac {S\{A\}}{S\{B\}}}}، أينأ،ب{\displaystyle A,B}وهي هياكل فرعية، وS{}{\displaystyle S\{\}}لا يُمثل هذا صيغةً مُحددة، بل هو إشارة إلى أن "أي سياق يُمكن إدراجه هنا". يُمكننا عرضه بصورة مُبسطة على النحو التالي:أب{\displaystyle {\frac {A}{B}}}مغادرةS{}{\displaystyle S\{\}}ضمني. بشكل افتراضي، يجب أن يكون للسياقات التي تظهر في قواعد الاستدلال قطبية موجبة.

للسياق قطبية . قطبية السياق إما إيجابية أو سلبية . على سبيل المثال،أ∨-{\displaystyle A\lor -}هو سياق إيجابي، لكنأ∨¬-{\displaystyle A\lor \neg -}هذا سياق سلبي، لكن(أ∨¬-)→ج{\displaystyle (A\lor \neg -)\to C}مرة أخرى، هذا سياق إيجابي. تُسمى إيجابية أو سلبية السياق بقطبيته . على سبيل المثال، نقول "أ∨-{\displaystyle A\lor -}له قطبية موجبة، وأ∨¬-{\displaystyle A\lor \neg -}له قطبية سالبة".

قد يكون هيكلان متناظرين لبعضهما البعض. وبالمثل، قد تكون قاعدتا استدلالS{أ}S{ب}،S{ب′}S{أ′}{\displaystyle {\frac {S\{A\}}{S\{B\}}},\;{\frac {S\{B'\}}{S\{A'\}}}}ويمكن أن تكون متناظرة مع بعضها البعض، إذا كان من الممكن كتابةأ′{\displaystyle A'}كبديل لـأ{\displaystyle A}، وب′{\displaystyle B'}كبديل لـب{\displaystyle B}. يُعدّ التضاد الكلاسيكي مثالاً على هذه الازدواجية.

من المتعارف عليه أن يكتب(){\displaystyle ()}للعطف، و[]{\displaystyle []}للفصل. على سبيل المثال، في المنطق الخطي، يكتب المرء(أ1،...،أن){\displaystyle (A_{1},\dots ,A_{n})}لأ1⊗⋯⊗أن{\displaystyle A_{1}\otimes \dots \otimes A_{n}}، و[أ1،...،أن]{\displaystyle [A_{1},\dots ,A_{n}]}لأ1⅋...⅋أن{\displaystyle A_{1}\mathbin {\mbox{⅋}} \dots \mathbin {\mbox{⅋}} A_{n}}.

أفكار

الاستدلال العميق

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

فعلى سبيل المثال، في حساب المتتاليات للمنطق الكلاسيكي، القاعدةΓ،أ،ب⊢ΔΓ،أ∧ب⊢Δ{\displaystyle {\frac {\Gamma ,A,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}}أوراقأ،ب{\displaystyle A,B}وجميع صيغها الفرعية دون تغيير. فقط الرابط المنطقي الخارجي لـأ∧ب{\displaystyle A\land B}يتم إنتاجه.

للاستدلال العميق، قد تنطبق قواعد الاستدلال على أي صيغة فرعية، مهما كان عمقها داخل شجرة بناء الجملة. بعبارة أخرى، من بين جميع العقد في شجرة بناء الجملة لـأ∧ب{\displaystyle A\land B}لا يمكن لقاعدة الاستدلال أن تعالج إلا العقدة الخارجية. أما الاستدلال العميق فيتيح للقاعدة معالجة أي عقدة داخل شجرة بناء الجملة.

التناظر من أعلى إلى أسفل

في حساب المتتابعات والاستدلال الطبيعي ، يُعرَّف البرهان بأنه شجرة من قواعد الاستدلال. وهذا يُنتج عدم تناظر جوهري: فقمة شجرة البرهان تتكون من العديد من المتتابعات الطرفية، بينما قاعدتها عبارة عن متتابعة طرفية واحدة. مع ذلك، فإن العديد من قواعد الاستدلال متناظرة: إذ يمكن استنتاج النصف العلوي والنصف السفلي بشكل متبادل.

على سبيل المثال، إذا كان بإمكان المرء تطبيق قاعدةΓ⊢أΓ⊢بΓ⊢أوب(⊢و){\displaystyle {\frac {\Gamma \vdash A\quad \Gamma \vdash B}{\Gamma \vdash A\&B}}(\vdash \&)}لتقديم دليل علىΓ⊢أوب{\displaystyle \Gamma \vdash A\&B}ثم يمكن للمرء أيضاً تقديم برهان علىΓ⊢أ{\displaystyle \Gamma \vdash A}وبرهان علىΓ⊢ب{\displaystyle \Gamma \vdash B}وبهذه الطريقة، قاعدة الاستدلال⊢و{\displaystyle \vdash \&}يتمتع بتناظر من أعلى إلى أسفل.

إنّ الشكلية في حساب المتتاليات تجعل هذا التناظر من أعلى إلى أسفل ضمنيًا، نظرًا لأنّ تجاور المتتاليةΓ⊢أ{\displaystyle \Gamma \vdash A}وتسلسل آخرΓ⊢ب{\displaystyle \Gamma \vdash B}ليست متتابعة بحد ذاتها. هذا يعني أن هذا التناظر من أعلى إلى أسفل ليس على مستوى الكائن في حساب البرهان .

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

إس كيه إس جي

تعريف

SKSg هو CoS لمنطق القضايا الكلاسيكي.

تتكون رموز SKSg مما يلي:

  • الذراتأ0،أ¯0،أ1،أ¯1،...{\displaystyle a_{0},{\bar {a}}_{0},a_{1},{\bar {a}}_{1},\dots }نقول ذلكأأنا،أ¯أنا{\displaystyle a_{i},{\bar {a}}_{i}}هي ذرات مزدوجة بالنسبة لبعضها البعض.
  • الروابط∨،∧{\displaystyle \lor ,\land }.
  • الوحدات⊤،⊥{\displaystyle \top ,\bot }.

لا يوجد نفي في SKSg، لأننا خفضنا النفي من رابط منطقي إلى مجرد اقتران بين الذرات المنطقية.

يحتوي هيكل SKSg على الصيغة النحوية التالية في شكل باكوس-ناور :F::=أ|أ¯|⊤|⊥|F∨F|F∧F{\displaystyle F::=a|{\bar {a}}|\top |\bot |F\lor F|F\land F}بدون النفي، تكون جميع السياقات إيجابية.

تُعرَّف الازدواجية في الهياكل بما يلي:أ¯=أ¯،أ¯¯=أأ∧ب¯=أ¯∨ب¯،أ∨ب¯=أ¯∧ب¯{\displaystyle {\begin{aligned}{\overline {a}}={\bar {a}},&\quad {\overline {\bar {a}}}=a\\{\overline {A\land B}}={\overline {A}}\lor {\overline {B}},&\quad {\overline {A\lor B}}={\overline {A}}\land {\overline {B}}\end{aligned}}}تأتي قواعد الاستدلال الهيكلي في 3 أزواج ثنائية :

⊤أ∨أ¯(أنا↓){\displaystyle {\frac {\top }{a\lor {\bar {a}}}}\;(\mathrm {i} \downarrow )}⊥أ(w↓){\displaystyle {\frac {\bot }{a}}\;(\mathrm {w} \downarrow )}أ∨أأ(ج↓){\displaystyle {\frac {a\lor a}{a}}\;(\mathrm {c} \downarrow )}
هويةإضعافانقباض
أ∧أ¯⊥(أنا↑){\displaystyle {\frac {a\land {\bar {a}}}{\bot }}\;(\mathrm {i} \uparrow )}أ⊤(w↑){\displaystyle {\frac {a}{\top }}\;(\mathrm {w} \uparrow )}أأ∧أ(ج↑){\displaystyle {\frac {a}{a\land a}}\;(\mathrm {c} \uparrow )}
يقطعاستيقاظ البقرالانقباض المشترك

قاعدتا الاستدلال المنطقي هما قاعدتان متناظرتان ذاتيًا:

أ∧(ب∨ج)(أ∧ب)∨ج(s){\displaystyle {\frac {A\land (B\lor C)}{(A\land B)\lor C}}\;(\mathrm {s} )}(أ∧ب)∨(ج∧د)(أ∨ج)∧(ب∨د)(م){\displaystyle {\frac {(A\land B)\lor (C\land D)}{(A\lor C)\land (B\lor D)}}\;(\mathrm {m} )}
يُحوّلالوسطي

بالإضافة إلى هذه القواعد، توجد المعادلات التالية:أ∨ب=ب∨أأ∧ب=ب∧أ(أ∨ب)∨ج=أ∨(ب∨ج)(أ∧ب)∧ج=أ∧(ب∧ج)أ∨⊥=أأ∧⊤=أ⊤∨⊤=⊤⊥∧⊥=⊥{\displaystyle {\begin{array}{rcl}A\lor B&=&B\lor A\\A\land B&=&B\land A\\(A\lor B)\lor C&=&A\lor (B\lor C)\\(A\land B)\land C&=&A\land (B\land C)\end{array}}\qquad {\begin{array}{rcl}A\lor \bot &=&A\\A\land \top &=&A\\\top \lor \top &=&\top \\\bot \land \bot &=&\bot \end{array}}\quad }يمكن استبدال جميع معادلات نظام SKSg بقواعد استدلال. النظام الناتج الخالي من المعادلات هو SKS.

ملكيات

هذا استنتاج صحيح: (أ∨ب)∧أ‖((أ∨ب)∧أ)∧((أ∨ب)∧أ)≡((أأ∧أ(ج↑))∨(بب∧ب(ج↑))(أ∨ب)∧(أ∨ب)(م))∧(أأ∧أ(ج↑)).{\displaystyle {\begin{array}{c}(a\lor b)\land a\\\Vert \\((a\lor b)\land a)\land ((a\lor b)\land a)\end{array}}\equiv \left({\frac {\left({\frac {a}{a\land a}}\;(\mathrm {c} \uparrow )\right)\lor \left({\frac {b}{b\land b}}\;(\mathrm {c} \uparrow )\right)}{(a\lor b)\land (a\lor b)}}\;(\mathrm {m} )\right)\land \left({\frac {a}{a\land a}}\;(\mathrm {c} \uparrow )\right)\quad .}هذا مبدأ عام في الاستدلال العميق: قاعدة هيكليةيمكن استبدال القواعد البنائية العامة بنفس القاعدة البنائية على الذرات. في هذه الحالة، يحدث انكماش مشترك.

الاشتقاق الخالي من القطع هو اشتقاق حيثأنا↑{\displaystyle \mathrm {i} \uparrow }لا يُستخدم. يمكن تجنب القطع بتقنية تُسمى التقسيم . [ 3 ] [ 4 ]

MLL⁻

عرّف MLL⁻ بأنه نظام إثبات المنطق الخطي المضاعف بدون وحدات .

تتكون الصيغة منF::=أ|أ¯|F⅋F|F×F{\displaystyle F::=a|{\bar {a}}|F\mathbin {\mbox{⅋}} F|F\times F}. هنا،أ{\displaystyle a}وأ¯{\displaystyle {\bar {a}}}هي ذرات ثنائية. معادلات الازدواجية هي(أ⊗ب)⊥=أ⊥⅋ب⊥،(أ⅋ب)⊥=أ⊥⊗ب⊥{\displaystyle (A\otimes B)^{\bot }=A^{\bot }\mathbin {\mbox{⅋}} B^{\bot },\quad (A\mathbin {\mbox{⅋}} B)^{\bot }=A^{\bot }\otimes B^{\bot }}على وجه الخصوص، لم يعد النفي موجودًا، لأننا خفضنا من شأن النفي من رابط منطقي إلى مجرد ثنائية بين أزواج من الذرات المنطقية. بحسب التعريف،أ¯¯=أ{\displaystyle {\bar {\bar {a}}}=a}.

يحتوي النظام على CoS التالي: [ 4 ]أنا↓أ⊥⅋أأنا↑أ⊗أ⊥أنا↓S{ب}S{(أ⊥⅋أ)⊗ب}أنا↑S{ب⅋(أ⊗أ⊥)}S{ب}σ↓S{أ⅋ب}S{ب⅋أ}σ↑S{أ⊗ب}S{ب⊗أ}α↓S{أ⅋(ب⅋ج)}S{(أ⅋ب)⅋ج}α↑S{أ⊗(ب⊗ج)}S{(أ⊗ب)⊗ج}sS{أ⊗(ب⅋ج)}S{(أ⊗ب)⅋ج}{\displaystyle {\begin{aligned}&\mathrm {i} \downarrow \;{\frac {}{A^{\perp }\mathbin {\mbox{⅋}} A}}&&\mathrm {i} \uparrow \;{\frac {A\otimes A^{\perp }}{}}\\&\mathrm {i} \downarrow \;{\frac {S\{B\}}{S\{(A^{\perp }\mathbin {\mbox{⅋}} A)\otimes B\}}}&&\mathrm {i} \uparrow \;{\frac {S\{B\mathbin {\mbox{⅋}} (A\otimes A^{\perp })\}}{S\{B\}}}\\&\sigma \downarrow \;{\frac {S\{A\mathbin {\mbox{⅋}} B\}}{S\{B\mathbin {\mbox{⅋}} A\}}}&&\sigma \uparrow \;{\frac {S\{A\otimes B\}}{S\{B\otimes A\}}}\\&\alpha \downarrow \;{\frac {S\{A\mathbin {\mbox{⅋}} (B\mathbin {\mbox{⅋}} C)\}}{S\{(A\mathbin {\mbox{⅋}} B)\mathbin {\mbox{⅋}} C\}}}&&\alpha \uparrow \;{\frac {S\{A\otimes (B\otimes C)\}}{S\{(A\otimes B)\otimes C\}}}\\&\mathrm {s} \;{\frac {S\{A\otimes (B\mathbin {\mbox{⅋}} C)\}}{S\{(A\otimes B)\mathbin {\mbox{⅋}} C\}}}\end{aligned}}}كل صف يمثل زوجًا من القواعد المزدوجة. قاعدة التبديل مزدوجة مع نفسها.

توجد أربع قواعد بدء، اثنتان لزيادة i، واثنتان لخفض i. والسبب في وجود اثنتين بدلاً من واحدة هو أن النظام لا يحتوي على وحدات.1،⊥{\displaystyle 1,\bot }مع الوحدة1{\displaystyle 1}ل⊗{\displaystyle \otimes }يمكن للمرء ببساطة أن يدمجأ⊥⅋أ{\displaystyle {\frac {}{A^{\perp }\mathbin {\mbox{⅋}} A}}}كحالة خاصة منS{ب}S{(أ⊥⅋أ)⊗ب}{\displaystyle {\frac {S\{B\}}{S\{(A^{\perp }\mathbin {\mbox{⅋}} A)\otimes B\}}}}، أينS{-}{\displaystyle S\{-\}}السياق فارغ، وب=1{\displaystyle B=1}وبالمثل، مع الوحدة⊥{\displaystyle \bot }ل⅋{\displaystyle \mathbin {\mbox{⅋}} }يمكن للمرء أن يدمجأ⊗أ⊥{\displaystyle {\frac {A\otimes A^{\bot }}{}}}تحتS{ب⅋(أ⊗أ⊥)}S{ب}{\displaystyle {\frac {S\{B\mathbin {\mbox{⅋}} (A\otimes A^{\perp })\}}{S\{B\}}}}.

قواعد تأسيس الجمعياتα{\displaystyle \alpha }والتبادلσ{\displaystyle \sigma }هذا يعني أن كلا الرابطين تجميعيان وتبديليان. يمكن استبدال هذه القواعد بالمعادلات(أ⊗ب)⊗ج=أ⊗(ب⊗ج){\displaystyle (A\otimes B)\otimes C=A\otimes (B\otimes C)}، إلخ.

يتوافق i↑ مع بديهية الهوية في حساب المتتابعات:أ⊢أ{\displaystyle A\vdash A}أو ما يعادل ذلك،⊢أ⊥،أ{\displaystyle \vdash A^{\bot },A}.

i↓ يتوافق مع قاعدة القطع:Γ⊢Δ،أأ،Γ′⊢Δ′Γ،Γ′⊢Δ،Δ′{\displaystyle {\frac {\Gamma \vdash \Delta ,A\quad A,\Gamma '\vdash \Delta '}{\Gamma ,\Gamma '\vdash \Delta ,\Delta '}}}.

قاعدة التبديلS{أ⊗(ب⅋ج)}S{(أ⊗ب)⅋ج}{\displaystyle {\frac {S\{A\otimes (B\mathbin {\mbox{⅋}} C)\}}{S\{(A\otimes B)\mathbin {\mbox{⅋}} C\}}}}الأمر أكثر دقة. وهو يتوافق معS{أ⊗(ب⅋ج)}⊢S{(أ⊗ب)⅋ج}{\displaystyle S\{A\otimes (B\mathbin {\mbox{⅋}} C)\}\vdash S\{(A\otimes B)\mathbin {\mbox{⅋}} C\}}بشكل عام، يمكن قراءة قاعدة الاستدلال لـ CoS على أنها متتالية قابلة للإثبات في حساب المتتاليات، عن طريق "تدويرها 90 درجة".

تفسير

في MLL⁻، الرموز⊗،⅋{\displaystyle \otimes ,\mathbin {\mbox{⅋}} }هي روابط منطقية (العطف، الفصل)، ولا تظهر إلا على مستوى الصيغ. أما على مستوى المتتاليات، فتتصرف الفاصلة بشكل أساسي بنفس طريقة⅋{\displaystyle \mathbin {\mbox{⅋}} }بما أن لدينا قاعدة الاستدلال التالية⊢Γ،أ،ب،Δ⊢Γ،أ⅋ب،Δ{\displaystyle {\frac {\vdash \Gamma ,A,B,\Delta }{\vdash \Gamma ,A\mathbin {\mbox{⅋}} B,\Delta }}}لكنها تظهر على مستوى المتتاليات. وبالمثل، فإن كتابة متتاليتين جنبًا إلى جنب داخل شجرة إثبات لها نفس السلوك تقريبًا كما⊗{\displaystyle \otimes }بما أن لدينا قاعدة الاستدلال التالية⊢Γ،أ⊢ب،Δ⊢Γ،أ⊗ب،Δ{\displaystyle {\frac {\vdash \Gamma ,A\quad \vdash B,\Delta }{\vdash \Gamma ,A\otimes B,\Delta }}}لكن ذلك يظهر على مستوى البراهين.

في قانون الأنظمة لـ MLL⁻، الرمز⊗{\displaystyle \otimes }يتم التعامل معها وفقًا لقواعد بحيث يمكنها القيام بوظيفة كل من الرابط المنطقي⊗{\displaystyle \otimes }والوضع المتسلسل جنبًا إلى جنب. وبالمثل بالنسبة لـ⅋{\displaystyle \mathbin {\mbox{⅋}} }.

على وجه الخصوص، إذا تم إعطاء شجرة إثبات في حساب التفاضل والتكامل المتتالي MLL⁻، فيمكن تحويلها إلى إثبات في MLL⁻ CoS إذا تم تحويل كل متتالية⊢أ1،...،أن{\displaystyle \vdash A_{1},\dots ,A_{n}}داخلأ1⅋...⅋أن{\displaystyle A_{1}\mathbin {\mbox{⅋}} \dots \mathbin {\mbox{⅋}} A_{n}}ثم قم بتحويل كل وضع متجاور للتسلسلات.⊢Γ1...⊢Γن{\displaystyle \vdash \Gamma _{1}\quad \dots \quad \vdash \Gamma _{n}}معΓ1⊗⋯⊗Γن{\displaystyle \Gamma _{1}\otimes \dots \otimes \Gamma _{n}}ثم استبدل كل استخدام لقاعدة الاستدلال في حساب المتتاليات باستخدام عدة قواعد استدلال في حساب التفاضل والتكامل. وهذا يُظهر أن البنى ليست مجرد تكرار للصيغ أو المتتاليات، لأنها تجمع بين خصائص كليهما.

يتوافق حذف القطع مع حذف i↓.

SLLS

نظام SLLS هو نسخة CoS من المنطق الخطي الكامل . وهو أكبر بكثير من CoS الخاص بـ MLL⁻. [ 5 ]أأنا↓1أ⅋أ¯أأنا↑أ⊗أ¯⊥د↓(أ⅋ب)و(ج⅋د)(أوج)⅋(ب⊕د)د↑(أ⊕ب)⊗(جود)(أ⊗ج)⊕(ب⊗د)ص↓!(R⅋تي)!R⅋؟تيص↑!R⊗؟تي؟(R⊗تي)أw↓0أأج↓أ⊕أأأج↑أأوأأw↑أ⊤نم↓00و0s(أ⅋ب)⊗ج(أ⊗ج)⅋بم(أوب)⊕(جود)(أ⊕ج)و(ب⊕د)نم↑⊤⊕⊤⊤نم1↓00⅋0م1↓(أ⅋ب)⊕(ج⅋د)(أ⊕ج)⅋(ب⊕د)م1↑(أوب)⊗(جود)(أ⊗ج)و(ب⊗د)نم1↑⊤⊗⊤⊤نم2↓00⊗0م2↓(أ⊗ب)⊕(ج⊗د)(أ⊕ج)⊗(ب⊕د)م2↑(أوب)⅋(جود)(أ⅋ج)و(ب⅋د)نم2↑⊤⅋⊤⊤نل1↓0؟0ل1↓؟R⊕؟تي؟(R⊕تي)ل1↑!(Rوتي)!Rو!تينل1↑!⊤⊤نل2↓0!0ل2↓!R⊕!تي!(R⊕تي)ل2↑؟(Rوتي)؟Rو؟تينل2↑؟⊤⊤نz↓⊥؟0z↓؟R⅋تي؟(R⊕تي)z↑!(Rوتي)!R⊗تينz↑!⊤1{\displaystyle {\begin{aligned}&\mathrm {ai} \downarrow \;{\frac {1}{a\mathbin {\mbox{⅋}} {\bar {a}}}}&&\mathrm {ai} \uparrow \;{\frac {a\otimes {\bar {a}}}{\bot }}\\&\mathrm {d} \downarrow \;{\frac {(A\mathbin {\mbox{⅋}} B)\mathbin {\&} (C\mathbin {\mbox{⅋}} D)}{(A\mathbin {\&} C)\mathbin {\mbox{⅋}} (B\oplus D)}}&&\mathrm {d} \uparrow \;{\frac {(A\oplus B)\otimes (C\mathbin {\&} D)}{(A\otimes C)\oplus (B\otimes D)}}\\&\mathrm {p} \downarrow \;{\frac {!(R\mathbin {\mbox{⅋}} T)}{!R\mathbin {\mbox{⅋}} ?T}}&&\mathrm {p} \uparrow \;{\frac {!R\otimes ?T}{?(R\otimes T)}}\\&\mathrm {aw} \downarrow \;{\frac {0}{a}}&&\mathrm {ac} \downarrow \;{\frac {a\oplus a}{a}}&&\mathrm {ac} \uparrow \;{\frac {a}{a\mathbin {\&} a}}&&\mathrm {aw} \uparrow \;{\frac {a}{\top }}\\&\mathrm {nm} \downarrow \;{\frac {0}{0\mathbin {\&} 0}}&&\mathrm {s} \;{\frac {(A\mathbin {\mbox{⅋}} B)\otimes C}{(A\otimes C)\mathbin {\mbox{⅋}} B}}&&\mathrm {m} \;{\frac {(A\mathbin {\&} B)\oplus (C\mathbin {\&} D)}{(A\oplus C)\mathbin {\&} (B\oplus D)}}&&\mathrm {nm} \uparrow \;{\frac {\top \oplus \top }{\top }}\\&\mathrm {nm} _{1}\downarrow \;{\frac {0}{0\mathbin {\mbox{⅋}} 0}}&&\mathrm {m} _{1}\downarrow \;{\frac {(A\mathbin {\mbox{⅋}} B)\oplus (C\mathbin {\mbox{⅋}} D)}{(A\oplus C)\mathbin {\mbox{⅋}} (B\oplus D)}}&&\mathrm {m} _{1}\uparrow \;{\frac {(A\mathbin {\&} B)\otimes (C\mathbin {\&} D)}{(A\otimes C)\mathbin {\&} (B\otimes D)}}&&\mathrm {nm} _{1}\uparrow \;{\frac {\top \otimes \top }{\top }}\\&\mathrm {nm} _{2}\downarrow \;{\frac {0}{0\otimes 0}}&&\mathrm {m} _{2}\downarrow \;{\frac {(A\otimes B)\oplus (C\otimes D)}{(A\oplus C)\otimes (B\oplus D)}}&&\mathrm {m} _{2}\uparrow \;{\frac {(A\mathbin {\&} B)\mathbin {\mbox{⅋}} (C\mathbin {\&} D)}{(A\mathbin {\mbox{⅋}} C)\mathbin {\&} (B\mathbin {\mbox{⅋}} D)}}&&\mathrm {nm} _{2}\uparrow \;{\frac {\top \mathbin {\mbox{⅋}} \top }{\top }}\\&\mathrm {nl} _{1}\downarrow \;{\frac {0}{?0}}&&\mathrm {l} _{1}\downarrow \;{\frac {?R\oplus ?T}{?(R\oplus T)}}&&\mathrm {l} _{1}\uparrow \;{\frac {!(R\mathbin {\&} T)}{!R\mathbin {\&} !T}}&&\mathrm {nl} _{1}\uparrow \;{\frac {!\top }{\top }}\\&\mathrm {nl} _{2}\downarrow \;{\frac {0}{!0}}&&\mathrm {l} _{2}\downarrow \;{\frac {!R\oplus !T}{!(R\oplus T)}}&&\mathrm {l} _{2}\uparrow \;{\frac {?(R\mathbin {\&} T)}{?R\mathbin {\&} ?T}}&&\mathrm {nl} _{2}\uparrow \;{\frac {?\top }{\top }}\\&\mathrm {nz} \downarrow \;{\frac {\bot }{?0}}&&\mathrm {z} \downarrow \;{\frac {?R\mathbin {\mbox{⅋}} T}{?(R\oplus T)}}&&\mathrm {z} \uparrow \;{\frac {!(R\mathbin {\&} T)}{!R\otimes T}}&&\mathrm {nz} \uparrow \;{\frac {!\top }{1}}\end{aligned}}}

أ⊗ب=ب⊗أ(أ⊗ب)⊗ج=أ⊗(ب⊗ج)أ⊗1=أأوب=بوأ(أوب)وج=أو(بوج)أو⊤=أأ⊕ب=ب⊕أ(أ⊕ب)⊕ج=أ⊕(ب⊕ج)أ⊕0=أأ⅋ب=ب⅋أ(أ⅋ب)⅋ج=أ⅋(ب⅋ج)أ⅋1=⊥؟؟R=؟R!!R=!R⊥⊕⊥=⊥=؟⊥1و1=1=!1{\displaystyle {\begin{aligned}A\otimes B&=B\otimes A&\qquad (A\otimes B)\otimes C&=A\otimes (B\otimes C)&\qquad A\otimes 1&=A\\A\mathbin {\&} B&=B\mathbin {\&} A&(A\mathbin {\&} B)\mathbin {\&} C&=A\mathbin {\&} (B\mathbin {\&} C)&A\mathbin {\&} \top &=A\\A\oplus B&=B\oplus A&(A\oplus B)\oplus C&=A\oplus (B\oplus C)&A\oplus 0&=A\\A\mathbin {\mbox{⅋}} B&=B\mathbin {\mbox{⅋}} A&(A\mathbin {\mbox{⅋}} B)\mathbin {\mbox{⅋}} C&=A\mathbin {\mbox{⅋}} (B\mathbin {\mbox{⅋}} C)&A\mathbin {\mbox{⅋}} 1&=\bot \\??R&=?R&!!R&=!R\\\bot \oplus \bot &=\bot =?\bot &1\mathbin {\&} 1&=1=!1\end{aligned}}}

بي في

يمكن إنتاج نظام BV (النظام الأساسي الخامس) بواسطة CoS هذا: [ 1 ]أأنا↓∘أ⅋أ¯أأنا↑أ⊗أ¯∘s(أ⅋ب)⊗ج(أ⊗ج)⅋بq↓(أ⅋ب)◃(ج⅋د)(أ◃ج)⅋(ب◃د)q↑(أ◃ب)⊗(ج◃د)(أ⊗ج)◃(ب⊗د){\displaystyle {\begin{aligned}&\mathrm {ai} \downarrow \;{\frac {\circ }{a\mathbin {\mbox{⅋}} {\bar {a}}}}&&\mathrm {ai} \uparrow \;{\frac {a\otimes {\bar {a}}}{\circ }}\\&\mathrm {s} \;{\frac {(A\mathbin {\mbox{⅋}} B)\otimes C}{(A\otimes C)\mathbin {\mbox{⅋}} B}}\\&\mathrm {q} \downarrow \;{\frac {(A\mathbin {\mbox{⅋}} B)\triangleleft (C\mathbin {\mbox{⅋}} D)}{(A\triangleleft C)\mathbin {\mbox{⅋}} (B\triangleleft D)}}&&\mathrm {q} \uparrow \;{\frac {(A\triangleleft B)\otimes (C\triangleleft D)}{(A\otimes C)\triangleleft (B\otimes D)}}\end{aligned}}}

أ⊗ب=ب⊗أ(أ⊗ب)⊗ج=أ⊗(ب⊗ج)أ⊗∘=أأ⅋ب=ب⅋أ(أ⅋ب)⅋ج=أ⅋(ب⅋ج)أ⅋∘=أ(أ◃ب)◃ج=أ◃(ب◃ج)أ◃∘=أ=∘◃أ{\displaystyle {\begin{aligned}A\otimes B&=B\otimes A&\qquad (A\otimes B)\otimes C&=A\otimes (B\otimes C)&\qquad A\otimes \circ &=A\\A\mathbin {\mbox{⅋}} B&=B\mathbin {\mbox{⅋}} A&(A\mathbin {\mbox{⅋}} B)\mathbin {\mbox{⅋}} C&=A\mathbin {\mbox{⅋}} (B\mathbin {\mbox{⅋}} C)&A\mathbin {\mbox{⅋}} \circ &=A\\&&(A\triangleleft B)\triangleleft C&=A\triangleleft (B\triangleleft C)&A\triangleleft \circ &=A=\circ \triangleleft A\end{aligned}}}

مراجع

  1. 1 2 غولييلمي، أليسيو (2007-01-01). "نظام التفاعل والبنية" . معاملات ACM في منطق الحوسبة . 8 (1): 1–es. arXiv : cs/9910023 . doi : 10.1145/1182613.1182614 . ISSN 1529-3785 . 
  2. ↑ نوفاكوفيتش، نوفاك؛ ستراسبورغر، لوتز (21-04-2015). "حول قوة الاستبدال في حساب البنى" . مجلة ACM للمعاملات في منطق الحاسوب . 16 (3): 19:1–19:20. doi : 10.1145/2701424 . ISSN 1529-3785 . 
  3. ↑ "الاستدلال العميق" . alessio.guglielmi.name . تم الاطلاع عليه بتاريخ 30-04-2026 .
  4. 1 2 ستراسبرغر، لوتز (2006-11-20). "شبكات البرهان وهوية البراهين". arXiv : cs/0610123 .
  5. ↑ ألير توبيلا، أندريا؛ ستراسبورغر، لوتز (2019). مقدمة في الاستدلال العميق: ملاحظات المحاضرة لمؤتمر ESSLLI'19، 5-16 أغسطس 2019، جامعة لاتفيا (PDF) (تقرير).

للمزيد من القراءة

  • كاي برونلر (2004). الاستدلال العميق والتناظر في البراهين الكلاسيكية . دار نشر لوغوس.