شبكة واقية

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

على سبيل المثال، هذان البرهانان المنطقيان الخطيان متطابقان:

${\displaystyle \vdash }$أ ، ب ، ج ، د ${\displaystyle \vdash }$أ ⅋ ب ، ج ، د ${\displaystyle \vdash }$أ ⅋ ب ، ج ⅋ د

${\displaystyle \vdash }$أ ، ب ، ج ، د ${\displaystyle \vdash }$أ ، ب ، ج ، د ${\displaystyle \vdash }$أ ⅋ ب ، ج ⅋ د

وستكون شبكاتهم المقابلة متطابقة.

تُعرف عدة معايير للتحقق من صحة بنية البرهان التسلسلي (أي ما يبدو كشبكة برهان) للتأكد من أنها في الواقع بنية برهان ملموسة (أي ما يشفر استنتاجًا صحيحًا في المنطق الخطي). أول هذه المعايير هو معيار الرحلة الطويلة ، ^{[ 1 ]} الذي وصفه جان إيف جيرار .

• المنطق الخطي
• لوديكس
• هندسة التفاعل
• فضاء متماسك
• الاستدلال العميق
• شبكات التفاعل

• البراهين والأنواع . جيرارد جي واي، لافونت واي، وتايلور بي. مطبعة كامبريدج، 1989.
• روبرتو دي كوزمو وفنسنت دانوس، كتاب المنطق الخطي التمهيدي
• شون أ. فولوب، دراسة استقصائية لشبكات ومصفوفات البرهان لمنطق البنية الفرعية