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

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

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

التعريفات

الصيغة هي سلسلة ( سليمة التكوين ) من الرموز المنطقية. على سبيل المثال ، $((a\land b)\land \neg c)\lor d$ هي صيغة.

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

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

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

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

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

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

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

أفكار

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

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

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

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

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

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

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

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

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

إس كيه إس جي

تعريف

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

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

الذرات $a_{0},{\bar {a}}_{0},a_{1},{\bar {a}}_{1},\dots$ نقول ذلك $a_{i},{\bar {a}}_{i}$ هي ذرات مزدوجة بالنسبة لبعضها البعض.
الروابط $\lor ,\land$ .
الوحدات $\top ,\bot$ .

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

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

تُعرَّف الازدواجية في الهياكل بما يلي: ${\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 أزواج ثنائية :

${\frac {\top }{a\lor {\bar {a}}}}\;(\mathrm {i} \downarrow )$	${\frac {\bot }{a}}\;(\mathrm {w} \downarrow )$	${\frac {a\lor a}{a}}\;(\mathrm {c} \downarrow )$
هوية	إضعاف	انقباض
${\frac {a\land {\bar {a}}}{\bot }}\;(\mathrm {i} \uparrow )$	${\frac {a}{\top }}\;(\mathrm {w} \uparrow )$	${\frac {a}{a\land a}}\;(\mathrm {c} \uparrow )$
يقطع	استيقاظ البقر	الانقباض المشترك

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

${\frac {A\land (B\lor C)}{(A\land B)\lor C}}\;(\mathrm {s} )$	${\frac {(A\land B)\lor (C\land D)}{(A\lor C)\land (B\lor D)}}\;(\mathrm {m} )$
يُحوّل	الوسطي

بالإضافة إلى هذه القواعد، توجد المعادلات التالية: ${\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.

ملكيات

هذا استنتاج صحيح: ${\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 .$ هذا مبدأ عام في الاستدلال العميق: قاعدة هيكليةيمكن استبدال القواعد البنائية العامة بنفس القاعدة البنائية على الذرات. في هذه الحالة، يحدث انكماش مشترك.

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

MLL⁻

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

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

يحتوي النظام على CoS التالي: ^{[ 4 ]} ${\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,\bot$ مع الوحدة $1$ ل $\otimes$ يمكن للمرء ببساطة أن يدمج ${\frac {}{A^{\perp }\mathbin {\mbox{⅋}} A}}$ كحالة خاصة من ${\frac {S\{B\}}{S\{(A^{\perp }\mathbin {\mbox{⅋}} A)\otimes B\}}}$ ، أين $S\{-\}$ السياق فارغ، و $B=1$ وبالمثل، مع الوحدة $\bot$ ل $\mathbin {\mbox{⅋}}$ يمكن للمرء أن يدمج ${\frac {A\otimes A^{\bot }}{}}$ تحت ${\frac {S\{B\mathbin {\mbox{⅋}} (A\otimes A^{\perp })\}}{S\{B\}}}$ .

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

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

i↓ يتوافق مع قاعدة القطع: ${\frac {\Gamma \vdash \Delta ,A\quad A,\Gamma '\vdash \Delta '}{\Gamma ,\Gamma '\vdash \Delta ,\Delta '}}$ .

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

تفسير

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

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

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

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

SLLS

نظام SLLS هو نسخة CoS من المنطق الخطي الكامل . وهو أكبر بكثير من CoS الخاص بـ MLL⁻. ^{[ 5 ]} ${\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}}$

${\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 ]} ${\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}}$

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

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

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

روابط خارجية

الصفحة الرئيسية لحساب التفاضل والتكامل الهيكلي
CoS in Maude : صفحة توثق تطبيقات الأنظمة المنطقية في حساب الهياكل، باستخدام نظام Maude .

[Guglielmi_1–es-1] 1 2 غولييلمي، أليسيو (2007-01-01). "نظام التفاعل والبنية" . معاملات ACM في منطق الحوسبة . 8 (1): 1–es. arXiv : cs/9910023 . doi : 10.1145/1182613.1182614 . ISSN 1529-3785 .

[:0-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 .

[:1-4] 1 2 ستراسبرغر، لوتز (2006-11-20). "شبكات البرهان وهوية البراهين". arXiv : cs/0610123 .

[5] ألير توبيلا، أندريا؛ ستراسبورغر، لوتز (2019). مقدمة في الاستدلال العميق: ملاحظات المحاضرة لمؤتمر ESSLLI'19، 5-16 أغسطس 2019، جامعة لاتفيا (PDF) (تقرير).

[ 1 ]

[ 3 ]

[ 5 ]