طريقة الجداول التحليلية

افترض مجموعة لانهائية${\displaystyle PV}$من المتغيرات الافتراضية وتحديد المجموعة${\displaystyle \Phi }$من الصيغ بالاستقراء، ممثلة بالقواعد النحوية التالية:

${\displaystyle \Phi$ ::=PV\mid \neg \Phi \mid (\Phi \to \Phi )\mid (\Phi \lor \Phi )\mid (\Phi \land \Phi )} .

أي أن الروابط الأساسية هي: النفي${\displaystyle \neg }$، دلالة${\displaystyle \to }$، الانفصال${\displaystyle \lor }$، والاقتران${\displaystyle \land }$.

تُسمى صحة أو خطأ الصيغة بقيمتها الصادقة. ويُقال إن الصيغة، أو مجموعة الصيغ، قابلة للتحقيق إذا كان هناك إمكانية لتعيين قيم صادقة للمتغيرات المنطقية بحيث تكون الصيغة بأكملها، التي تجمع المتغيرات مع الروابط المنطقية، صحيحة أيضًا. ^{[ 1 ]} ويُقال إن هذا التعيين يُحقق الصيغة. ^{[ 2 ]}

يتحقق الجدول مما إذا كانت مجموعة معينة من الصيغ قابلة للتحقيق أم لا. ويمكن استخدامه للتحقق من صحة الصيغة أو استلزامها: تكون الصيغة صحيحة إذا كان نفيها غير قابل للتحقيق، والصيغ الأخرى غير قابلة للتحقيق.${\displaystyle A_{1},\ldots ,A_{n}}$يعني${\displaystyle B}$لو${\displaystyle \{A_{1},\ldots ,A_{n},\neg B\}}$غير مُرضٍ.

لأي صيغ${\displaystyle X}$،${\displaystyle Y}$الحقائق التالية صحيحة:

• إذا كان حرف عطف${\displaystyle X\land Y}$    إذا كان ذلك صحيحاً، فإذن${\displaystyle X}$،${\displaystyle Y}$كلاهما صحيح؛ إذا كان خاطئًا، فإما    ${\displaystyle X}$خطأ أو${\displaystyle Y}$هذا غير صحيح.
• إذا حدث انفصال${\displaystyle X\lor Y}$    إذا كان ذلك صحيحاً، فإما${\displaystyle X}$صحيح أو${\displaystyle Y}$صحيح؛ خاطئ، إذن    ${\displaystyle X}$،${\displaystyle Y}$كلاهما خاطئ.
• إذا كان الشرط${\displaystyle X\to Y}$    إذا كان ذلك صحيحاً، فإما${\displaystyle X}$خطأ أو${\displaystyle Y}$صحيح؛ خاطئ، إذن    ${\displaystyle X}$صحيح و${\displaystyle Y}$هذا غير صحيح.
• إذا كان النفي${\displaystyle \neg X}$    إذا كان ذلك صحيحاً، فإذن${\displaystyle X}$خطأ؛ خطأ، إذن    ${\displaystyle X}$هذا صحيح.

تعتمد طريقة الجداول التحليلية على هذه الحقائق. ويتمثل المبدأ الأساسي للجداول المنطقية في محاولة "تقسيم" الصيغ المعقدة إلى صيغ أصغر حتى يتم إنتاج أزواج متكاملة من المتغيرات أو حتى يتعذر إجراء أي توسيع إضافي.

تعتمد هذه الطريقة على شجرة تُسمى عقدها بصيغ رياضية. في كل خطوة، تُعدّل هذه الشجرة؛ في حالة القضايا المنطقية، التغييرات المسموح بها هي إضافة عقدة كفرع من ورقة. تبدأ العملية بإنشاء الشجرة المكونة من سلسلة جميع الصيغ في المجموعة المراد إثبات عدم قابليتها للإرضاء. ^{[ 11 ]} بعد ذلك، يمكن تطبيق الإجراء التالي بشكل متكرر وغير حتمي:

1. اختر عقدة طرفية مفتوحة. (العقدة الطرفية في السلسلة الأولية مُعلّمة بأنها مفتوحة).
2. اختر عقدة مناسبة على الفرع الموجود أعلى العقدة المحددة. ^{[ 12 ]}
3. قم بتطبيق العقدة المناسبة، والتي تتوافق مع توسيع الشجرة أسفل عقدة الورقة المحددة بناءً على قاعدة توسيع معينة (مفصلة أدناه).
4. لكل عقدة جديدة يتم إنشاؤها وتكون حرفية/حرفية منفية، ويظهر مكملها في عقدة سابقة على نفس الفرع، ضع علامة على الفرع بأنه مغلق . ضع علامة على جميع العقد الأخرى التي تم إنشاؤها حديثًا بأنها مفتوحة .

إذا احتوى أحد فروع الجدول على صيغة ...

• ${\displaystyle {\boldsymbol {\mathsf {T}}}(X\land Y)}$أضف إلى ورقتها سلسلة من عقدتين تحتويان على الصيغ.${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$و${\displaystyle {\boldsymbol {\mathsf {T}}}(Y)}$; ^{[ 13 ]}
• ${\displaystyle {\boldsymbol {\mathsf {F}}}(X\land Y)}$أنشئ فرعين شقيقين لورقتها، يحتويان على الصيغ التالية:${\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$و${\displaystyle {\boldsymbol {\mathsf {F}}}(Y)}$على التوالي؛ ^{[ 14 ]}
• ${\displaystyle {\boldsymbol {\mathsf {T}}}(X\lor Y)}$أنشئ فرعين شقيقين لورقتها، يحتويان على الصيغ التالية:${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$و${\displaystyle {\boldsymbol {\mathsf {T}}}(Y)}$على التوالى؛
• ${\displaystyle {\boldsymbol {\mathsf {F}}}(X\lor Y)}$أضف إلى ورقتها سلسلة من عقدتين تحتويان على الصيغ.${\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$و${\displaystyle {\boldsymbol {\mathsf {F}}}(Y)}$؛
• ${\displaystyle {\boldsymbol {\mathsf {T}}}(X\to Y)}$أنشئ فرعين شقيقين لورقتها، يحتويان على الصيغ التالية:${\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$و${\displaystyle {\boldsymbol {\mathsf {T}}}(Y)}$على التوالى؛
• ${\displaystyle {\boldsymbol {\mathsf {F}}}(X\to Y)}$أضف إلى ورقتها سلسلة من عقدتين تحتويان على الصيغ.${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$و${\displaystyle {\boldsymbol {\mathsf {F}}}(Y)}$؛
• ${\displaystyle {\boldsymbol {\mathsf {T}}}(\neg X)}$أضف إلى ورقتها العقدة التي تحتوي على الصيغة${\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$؛
• ${\displaystyle {\boldsymbol {\mathsf {F}}}(\neg X)}$أضف إلى ورقتها العقدة التي تحتوي على الصيغة${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$.

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

${\displaystyle {\frac {{\boldsymbol {\mathsf {T}}}(X\land Y)}{\begin{array}{c}{\boldsymbol {\mathsf {T}}}(X)\\{\boldsymbol {\mathsf {T}}}(Y)\end{array}}}}$	${\displaystyle {\frac {{\boldsymbol {\mathsf {T}}}(X\lor Y)}{\begin{array}{c}{\boldsymbol {\mathsf {T}}}(X)\mid {\boldsymbol {\mathsf {T}}}(Y)\end{array}}}}$	${\displaystyle {\frac {{\boldsymbol {\mathsf {T}}}(X\to Y)}{\begin{array}{c}{\boldsymbol {\mathsf {F}}}(X)\mid {\boldsymbol {\mathsf {T}}}(Y)\end{array}}}}$	${\displaystyle {\frac {{\boldsymbol {\mathsf {T}}}(\neg X)}{\begin{array}{c}{\boldsymbol {\mathsf {F}}}(X)\end{array}}}}$
${\displaystyle {\frac {{\boldsymbol {\mathsf {F}}}(X\land Y)}{\begin{array}{c}{\boldsymbol {\mathsf {F}}}(X)\mid {\boldsymbol {\mathsf {F}}}(Y)\end{array}}}}$	${\displaystyle {\frac {{\boldsymbol {\mathsf {F}}}(X\lor Y)}{\begin{array}{c}{\boldsymbol {\mathsf {F}}}(X)\\{\boldsymbol {\mathsf {F}}}(Y)\end{array}}}}$	${\displaystyle {\frac {{\boldsymbol {\mathsf {F}}}(X\to Y)}{\begin{array}{c}{\boldsymbol {\mathsf {T}}}(X)\\{\boldsymbol {\mathsf {F}}}(Y)\end{array}}}}$	${\displaystyle {\frac {{\boldsymbol {\mathsf {F}}}(\neg X)}{\begin{array}{c}{\boldsymbol {\mathsf {T}}}(X)\end{array}}}}$

ملاحظة : في الأنظمة القائمة على القواعد النحوية

${\displaystyle \Phi$ ::=\bot \mid PV\mid (\Phi \to \Phi )\mid (\Phi \lor \Phi )\mid (\Phi \land \Phi )} ,

التي لا تتعامل مع النفي كخاصية أولية، بل تُعرّفه من حيث الاستلزام والزيف (${\displaystyle \neg \Phi \,{\overset {\text{def}}{=}}\,\Phi \to \bot }$)، قواعد الجدول لـ${\displaystyle \neg }$يتم استبدالها بـ

${\displaystyle {\boldsymbol {\mathsf {T}}}(\bot )}$	:	أغلق الفرع (تناقض)،
${\displaystyle {\boldsymbol {\mathsf {F}}}(\bot )}$	:	لا تفعل شيئًا (لأنه ببساطة لا يؤكد أي تناقض).

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

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

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

بمجرد احتواء فرع على حرف ونفيه، تصبح صيغته المقابلة غير قابلة للإرضاء. ونتيجة لذلك، يمكن "إغلاق" هذا الفرع، إذ لا حاجة لتوسيعه أكثر. إذا كانت جميع فروع جدول ما مغلقة، فإن الصيغة التي يمثلها الجدول تكون غير قابلة للإرضاء؛ وبالتالي، تكون المجموعة الأصلية غير قابلة للإرضاء أيضًا. يُعد الحصول على جدول تكون فيه جميع الفروع مغلقة طريقة لإثبات عدم قابلية المجموعة الأصلية للإرضاء. في حالة القضايا، يمكن أيضًا إثبات قابلية الإرضاء من خلال استحالة إيجاد جدول مغلق، شريطة تطبيق كل قاعدة توسيع في كل مكان يمكن تطبيقها فيه. على وجه الخصوص، إذا احتوى جدول ما على بعض الفروع المفتوحة (غير المغلقة) وتم استخدام كل صيغة ليست حرفًا بواسطة قاعدة لتوليد عقدة جديدة على كل فرع توجد فيه الصيغة، فإن المجموعة تكون قابلة للإرضاء.

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

يمكن تبسيط القواعد المذكورة أعلاه لجدول القضايا باستخدام الترميز الموحد. في الترميز الموحد، تكون كل صيغة إما من النوع${\displaystyle \alpha }$(ألفا) أو من النوع${\displaystyle \beta }$(بيتا). يتم تخصيص مكونين لكل صيغة من النوع ألفا${\displaystyle \alpha _{1},\alpha _{2}}$ويتم تخصيص المكونين لكل صيغة من النوع بيتا${\displaystyle \beta _{1},\beta _{2}}$يمكن اعتبار الصيغ من النوع ألفا صيغًا اقترانية، حيث أن كليهما${\displaystyle \alpha _{1}}$و${\displaystyle \alpha _{2}}$يُستدل على ذلك من خلال${\displaystyle \alpha }$كونها صحيحة. يمكن اعتبار الصيغ من النوع بيتا صيغًا منفصلة، ​​إما${\displaystyle \beta _{1}}$أو${\displaystyle \beta _{2}}$يُستدل على ذلك من خلال${\displaystyle \beta }$كونها صحيحة. توضح الجداول أدناه كيفية تحديد نوع ومكونات أي صيغة منطقية معينة . ^{[ 15 ]}

${\displaystyle {\begin{array}{c|c|c}\alpha &\alpha _{1}&\alpha _{2}\\\hline {\boldsymbol {\mathsf {T}}}(X\land Y)&{\boldsymbol {\mathsf {T}}}(X)&{\boldsymbol {\mathsf {T}}}(Y)\\{\boldsymbol {\mathsf {F}}}(X\lor Y)&{\boldsymbol {\mathsf {F}}}(X)&{\boldsymbol {\mathsf {F}}}(Y)\\{\boldsymbol {\mathsf {F}}}(X\to Y)&{\boldsymbol {\mathsf {T}}}(X)&{\boldsymbol {\mathsf {F}}}(Y)\\{\boldsymbol {\mathsf {T}}}(\neg X)&{\boldsymbol {\mathsf {F}}}(X)&{\boldsymbol {\mathsf {F}}}(X)\\{\boldsymbol {\mathsf {F}}}(\neg X)&{\boldsymbol {\mathsf {T}}}(X)&{\boldsymbol {\mathsf {T}}}(X)\\\end{array}}}$

${\displaystyle {\begin{array}{c|c|c}\beta &\beta _{1}&\beta _{2}\\\hline {\boldsymbol {\mathsf {F}}}(X\land Y)&{\boldsymbol {\mathsf {F}}}(X)&{\boldsymbol {\mathsf {F}}}(Y)\\{\boldsymbol {\mathsf {T}}}(X\lor Y)&{\boldsymbol {\mathsf {T}}}(X)&{\boldsymbol {\mathsf {T}}}(Y)\\{\boldsymbol {\mathsf {T}}}(X\to Y)&{\boldsymbol {\mathsf {F}}}(X)&{\boldsymbol {\mathsf {T}}}(Y)\\\end{array}}}$

في كل جدول، يعرض العمود الأيسر جميع الهياكل الممكنة للصيغ من النوع ألفا أو بيتا، بينما تعرض الأعمدة اليمنى مكوناتها الخاصة.

عند إنشاء جدول القضايا باستخدام الترميز المذكور أعلاه، كلما صادف المرء صيغة من النوع ألفا، فإن مكونيها${\displaystyle \alpha _{1},\alpha _{2}}$تُضاف إلى الفرع الحالي الذي يتم توسيعه. كلما صادف المرء صيغة من النوع بيتا في فرع ما${\displaystyle \theta }$يمكن للمرء أن ينقسم${\displaystyle \theta }$إلى فرعين، أحدهما يحتوي على المجموعة {${\displaystyle \theta }$،${\displaystyle \beta _{1}}$} من الصيغ، والآخر مع المجموعة {${\displaystyle \theta }$،${\displaystyle \beta _{2}}$} من الصيغ. ^{[ 16 ]}

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

يمكن الآن تطبيق قواعد توسيع الجدول على أوراق الجدول، متجاهلةً جميع العقد الداخلية. أما بالنسبة للاقتران، فتعتمد القاعدة على تكافؤ مجموعة تحتوي على اقتران.${\displaystyle A\land B}$مع احتواء المجموعة على كليهما${\displaystyle A}$و${\displaystyle B}$بدلاً من ذلك. على وجه الخصوص، إذا كانت الورقة تحمل علامة بـ${\displaystyle X\cup \{A\land B\}}$، ويمكن إضافة عقدة إليها مع تسمية${\displaystyle X\cup \{A,B\}}$:

${\displaystyle (\land ){\frac {X\cup \{A\land B\}}{X\cup \{A,B\}}}}$

بالنسبة للفصل، مجموعة${\displaystyle X\cup \{A\lor B\}}$يكافئ ذلك فصل المجموعتين${\displaystyle X\cup \{A\}}$و${\displaystyle X\cup \{B\}}$ونتيجة لذلك، إذا كانت المجموعة الأولى تُصنف ورقة، فيمكن إلحاق طفلين بها، ويتم تصنيفهما بالصيغتين الأخيرتين.

${\displaystyle (\lor ){\frac {X\cup \{A\lor B\}}{X\cup \{A\}|X\cup \{B\}}}}$

وأخيرًا، إذا احتوت المجموعة على كل من القيمة الحرفية ونفيها، فيمكن إغلاق هذا الفرع:

${\displaystyle (id){\frac {X\cup \{p,\neg p\}}{closed}}}$

الجدول لمجموعة منتهية معينة X هو شجرة منتهية (مقلوبة) جذرها X ، حيث تُستمد جميع العقد الفرعية بتطبيق قواعد الجدول على العقد الأبوية. يُقال إن فرعًا في هذا الجدول مغلق إذا احتوت عقدته الطرفية على كلمة "مغلق". ويُقال إن الجدول مغلق إذا كانت جميع فروعه مغلقة. ويُقال إن الجدول مفتوح إذا كان فرع واحد على الأقل غير مغلق.

فيما يلي لوحتان مغلقتان للمجموعة

${\displaystyle X=\{r\land \neg r,\;p\land ((\neg p\lor q)\land \neg q)\}}$

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

${\displaystyle {\dfrac {\quad {\dfrac {\quad r\land \neg r,\;p\land ((\neg p\lor q)\land \neg q)\quad }{r,\;\neg r,\;p\land ((\neg p\lor q)\land \neg q)}}(\land )}{closed}}(\land )}$

وثانياً، وهي أطول، مع تطبيق القواعد بترتيب مختلف:

${\displaystyle {\dfrac {\quad {\dfrac {\quad {\dfrac {\quad r\land \neg r,\;p\land ((\neg p\lor q)\land \neg q)\quad }{r\land \neg r,\;p,\;((\neg p\lor q)\land \neg q)}}(\land )\quad }{r\land \neg r,\;p,\;(\neg p\lor q),\;\neg q}}(\land )}{\quad {\dfrac {\quad r\land \neg r,\;p,\;\neg p,\;\neg q\quad }{closed}}(id)\quad \quad {\dfrac {\quad r\land \neg r,\;p,\;q,\;\neg q\quad }{closed}}(id)}}(\lor )}$

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

القواعد الثلاث${\displaystyle (\land )}$،${\displaystyle (\lor )}$و${\displaystyle (id)}$ما سبق يكفي لتحديد ما إذا كانت مجموعة معينة${\displaystyle X'}$الصيغ في شكلها الطبيعي المنفي قابلة للتحقيق بشكل مشترك:

ما عليك سوى تطبيق جميع القواعد الممكنة بجميع الترتيبات الممكنة حتى نجد جدولًا مغلقًا لـ${\displaystyle X'}$أو حتى نستنفد جميع الاحتمالات ونخلص إلى أن كل لوحة لـ${\displaystyle X'}$مفتوح.

في الحالة الأولى،${\displaystyle X'}$غير قابلة للحل بشكل مشترك، وفي الحالة الثانية، تعطي العقدة الطرفية للفرع المفتوح تعيينًا للصيغ الذرية والصيغ الذرية المنفية مما يجعل${\displaystyle X'}$قابلة للتحقيق بشكل مشترك. في الواقع، يتمتع المنطق الكلاسيكي بخاصية رائعة تتمثل في أننا نحتاج إلى فحص جدول واحد فقط (أي جدول) بشكل كامل: إذا كان الجدول مغلقًا، فإن${\displaystyle X'}$غير مُرضٍ، وإذا كان مفتوحًا...${\displaystyle X'}$قابلة للإرضاء. لكن هذه الخاصية لا تتمتع بها المنطق الأخرى بشكل عام.

تكفي هذه القواعد لجميع قواعد المنطق الكلاسيكي، وذلك بأخذ مجموعة أولية من الصيغ X واستبدال كل عنصر C بصيغته الطبيعية المنفية المكافئة منطقيًا C'، ما ينتج عنه مجموعة من الصيغ X' . نعلم أن X قابلة للإرضاء إذا وفقط إذا كانت X' قابلة للإرضاء، لذا يكفي البحث عن جدول مغلق لـ X' باستخدام الإجراء الموضح أعلاه.

عن طريق الضبط${\displaystyle X=\{\neg A\}}$يمكن للمرء أن يختبر ما إذا كانت الصيغة A عبارة عن تحصيل حاصل في المنطق الكلاسيكي:

إذا كان الجدول الزمني لـ${\displaystyle \{\neg A\}}$ثم يغلق${\displaystyle \neg A}$غير قابلة للإثبات، وبالتالي فإن A عبارة عن تحصيل حاصل، إذ لا يمكن لأي قيمة منطقية أن تجعل A خاطئة. وإلا، فإن أي ورقة مفتوحة من أي فرع مفتوح من أي جدول مفتوح لـ${\displaystyle \{\neg A\}}$يُعطي مهمة تُفنّد A.

صيغة من الدرجة الأولى${\displaystyle \forall x.\gamma (x)}$يشمل ذلك جميع الصيغ${\displaystyle \gamma (t)}$أين${\displaystyle t}$هو حد أساسي . وبالتالي فإن قاعدة الاستدلال التالية صحيحة:

${\displaystyle (\forall ){\frac {\forall x.\gamma (x)}{\gamma (t)}}}$أين${\displaystyle t}$هو مصطلح أساسي اعتباطي

على عكس قواعد الروابط المنطقية، قد يكون من الضروري تطبيق هذه القاعدة عدة مرات على الصيغة نفسها. على سبيل المثال، المجموعة${\displaystyle \{\neg P(a)\lor \neg P(b),\forall x.P(x)\}}$لا يمكن إثبات عدم إمكانية تحقيقها إلا إذا كان كلا${\displaystyle P(a)}$و${\displaystyle P(b)}$يتم توليدها من${\displaystyle \forall x.P(x)}$.

تُعالج المُكمِّمات الوجودية باستخدام عملية سكولمية. على وجه الخصوص، صيغة تحتوي على مُكمِّم وجودي رئيسي مثل${\displaystyle \exists x.\delta (x)}$يُنتج عملية سكولمية${\displaystyle \delta (c)}$، أين${\displaystyle c}$هو رمز ثابت جديد.

${\displaystyle (\exists ){\frac {\exists x.\delta (x)}{\delta (c)}}}$أين${\displaystyle c}$هو رمز ثابت جديد

مصطلح سكوليم${\displaystyle c}$هو ثابت (دالة من الرتبة 0) لأن التحديد الكمي على${\displaystyle x}$لا يقع ضمن نطاق أي مُكمِّم شامل. إذا احتوت الصيغة الأصلية على بعض المُكمِّمات الشاملة بحيث يكون التحديد الكمي على${\displaystyle x}$كانت هذه المحددات الكمية ضمن نطاقها، ومن الواضح أنها قد أزيلت بتطبيق قاعدة المحددات الكمية الشاملة.

تُدخل قاعدة المُكمِّمات الوجودية رموزًا ثابتة جديدة. ويمكن استخدام هذه الرموز بواسطة قاعدة المُكمِّمات الكلية، بحيث${\displaystyle \forall y.\gamma (y)}$يمكن أن يولد${\displaystyle \gamma (c)}$حتى لو${\displaystyle c}$لم يكن موجودًا في الصيغة الأصلية ولكنه ثابت سكوليم تم إنشاؤه بواسطة قاعدة الكميات الوجودية.

القاعدتان المذكورتان أعلاه للمُكمِّمات الكلية والوجودية صحيحتان، وكذلك القواعد الافتراضية: إذا ولّدت مجموعة من الصيغ جدولًا مغلقًا، فإن هذه المجموعة غير قابلة للإرضاء. ويمكن إثبات الاكتمال أيضًا: إذا كانت مجموعة من الصيغ غير قابلة للإرضاء، فإنه يوجد جدول مغلق مبني منها باستخدام هذه القواعد. ومع ذلك، فإن إيجاد مثل هذا الجدول المغلق يتطلب سياسة مناسبة لتطبيق القواعد. وإلا، فقد تُولِّد مجموعة غير قابلة للإرضاء جدولًا لا نهائي النمو. على سبيل المثال، المجموعة${\displaystyle \{\neg P(f(c)),\forall x.P(x)\}}$غير قابل للتنفيذ، ولكن لا يمكن الحصول على جدول مغلق إذا استمر المرء بشكل غير حكيم في تطبيق قاعدة الكميات الشاملة على${\displaystyle \forall x.P(x)}$، على سبيل المثال توليد${\displaystyle P(c),P(f(c)),P(f(f(c))),\ldots }$يمكن دائمًا العثور على جدول مغلق عن طريق استبعاد هذه السياسات "غير العادلة" المماثلة لتطبيق قواعد الجدول.

قاعدة الكميات الشاملة${\displaystyle (\forall )}$هذه القاعدة الوحيدة غير الحتمية، إذ لا تُحدد المصطلح الذي يجب استخدامه. علاوة على ذلك، بينما تُطبق القواعد الأخرى مرة واحدة فقط لكل صيغة ولكل مسار، قد تتطلب هذه القاعدة عدة تطبيقات. مع ذلك، يمكن تقييد تطبيق هذه القاعدة بتأخير تطبيقها حتى لا تنطبق أي قاعدة أخرى، وبتقييد تطبيقها على المصطلحات الأساسية التي تظهر بالفعل في مسار الجدول. يهدف شكل الجداول الموحد الموضح أدناه إلى حل مشكلة عدم الحتمية.

تكمن المشكلة الرئيسية في استخدام الجداول بدون توحيد في كيفية اختيار مصطلح أساسي${\displaystyle t}$بالنسبة لقاعدة المُكمِّم الشامل. في الواقع، يمكن استخدام كل مصطلح أساسي ممكن، ولكن من الواضح أن معظمها قد يكون غير مفيد لإغلاق الجدول.

يتمثل أحد حلول هذه المشكلة في "تأجيل" اختيار الحد إلى الوقت الذي تسمح فيه نتيجة القاعدة بإغلاق فرع واحد على الأقل من الجدول. ويمكن تحقيق ذلك باستخدام متغير بدلاً من حد، بحيث${\displaystyle \forall x.\gamma (x)}$يُنشئ${\displaystyle \gamma (x')}$ثم السماح بإجراء عمليات استبدال لاحقة${\displaystyle x'}$مع مصطلح. تصبح قاعدة المحددات الكمية الشاملة كما يلي:

${\displaystyle (\forall ){\frac {\forall x.\gamma (x)}{\gamma (x')}}}$أين${\displaystyle x'}$متغير لا يظهر في أي مكان آخر في الجدول

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

تستخدم هذه القاعدة متغيرًا بدلًا من حد أساسي. وتكمن الفائدة من هذا التغيير في إمكانية إعطاء هذه المتغيرات قيمة عند إغلاق فرع من الجدول، مما يحل مشكلة توليد حدود قد تكون غير مفيدة.

${\displaystyle (\sigma )}$

لو${\displaystyle \sigma }$هو أكثر أداة توحيد عامة بين حرفين${\displaystyle A}$و${\displaystyle B}$، أين${\displaystyle A}$ونفي${\displaystyle B}$يحدث في نفس فرع الجدول،${\displaystyle \sigma }$يمكن تطبيقها في نفس الوقت على جميع صيغ الجدول

على سبيل المثال،${\displaystyle \{\neg P(a),\forall x.P(x)\}}$يمكن إثبات عدم إمكانية تحقيقها عن طريق توليد${\displaystyle P(x_{1})}$نفي هذا الحرفي قابل للتوحيد مع${\displaystyle \neg P(a)}$وأكثر العوامل توحيدًا هو الاستبدال الذي يحل محل${\displaystyle x_{1}}$مع${\displaystyle a}$يؤدي تطبيق هذا الاستبدال إلى استبدال${\displaystyle P(x_{1})}$مع${\displaystyle P(a)}$، مما يختتم المشهد.

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

تُعالج المُكمِّمات الوجودية بواسطة عملية سكولم. على عكس الجدول بدون توحيد، قد لا تكون حدود سكولم ثوابت بسيطة. في الواقع، قد تحتوي الصيغ في جدول مع توحيد على متغيرات حرة، والتي تُعتبر ضمنيًا مُكمَّمة عالميًا. ونتيجة لذلك، فإن صيغة مثل${\displaystyle \exists x.\delta (x)}$قد يكون ضمن نطاق المحددات الكمية الشاملة؛ إذا كان الأمر كذلك، فإن مصطلح سكوليم ليس ثابتًا بسيطًا ولكنه مصطلح مكون من رمز دالة جديد والمتغيرات الحرة للصيغة.

${\displaystyle (\exists ){\frac {\exists x.\delta (x)}{\delta (f(x_{1},\ldots ,x_{n}))}}}$أين${\displaystyle f}$هو رمز دالة جديد و${\displaystyle x_{1},\ldots ,x_{n}}$المتغيرات الحرة لـ${\displaystyle \delta }$

تتضمن هذه القاعدة تبسيطًا مقارنةً بقاعدة أخرى حيث${\displaystyle x_{1},\ldots ,x_{n}}$المتغيرات الحرة للفرع، وليس للفرع نفسه.${\displaystyle \delta }$بمفرده. يمكن تبسيط هذه القاعدة أكثر بإعادة استخدام رمز الدالة إذا سبق استخدامه في صيغة مطابقة لـ${\displaystyle \delta }$حتى إعادة تسمية المتغيرات.

تُستنتج الصيغة المُمثلة بجدول بطريقة مشابهة للحالة الافتراضية، مع افتراض إضافي مفاده أن المتغيرات الحرة تُعتبر مُكمّمة بشكل شامل. وكما هو الحال في الحالة الافتراضية، تُربط الصيغ في كل فرع، وتُفصل الصيغ الناتجة. بالإضافة إلى ذلك، تُعتبر جميع المتغيرات الحرة في الصيغة الناتجة مُكمّمة بشكل شامل. جميع هذه المُكمّمات تشمل الصيغة بأكملها ضمن نطاقها. بعبارة أخرى، إذا${\displaystyle F}$هي الصيغة التي تم الحصول عليها بفصل الصيغ المتصلة في كل فرع، و${\displaystyle x_{1},\ldots ,x_{n}}$هل المتغيرات الحرة فيه؟${\displaystyle \forall x_{1},\ldots ,x_{n}.F}$الصيغة الممثلة في الجدول. تنطبق الاعتبارات التالية:

• إن افتراض أن المتغيرات الحرة قابلة للقياس الكمي بشكل شامل هو ما يجعل تطبيق الموحد الأكثر عمومية قاعدة سليمة: بما أن${\displaystyle \gamma (x')}$هذا يعني أن${\displaystyle \gamma }$هذا صحيح لكل قيمة ممكنة لـ${\displaystyle x'}$، ثم${\displaystyle \gamma (t)}$ينطبق هذا على المصطلح${\displaystyle t}$أن الموحد الأكثر عمومية يحل محل${\displaystyle x}$مع.
• المتغيرات الحرة في الجدول ثابتة: يجب استبدال جميع حالات ظهور المتغير نفسه بنفس الحد. يمكن اعتبار كل متغير رمزًا يمثل حدًا لم يُحدد بعد. هذا نتيجة لافتراض أن المتغيرات الحرة مُكمّمة بشكل شامل على الصيغة الكاملة التي يمثلها الجدول: إذا ظهر المتغير نفسه حرًا في عقدتين مختلفتين، فإن كلا الظهورين يقعان ضمن نطاق نفس المُكمّم. على سبيل المثال، إذا كانت الصيغ في عقدتين هما${\displaystyle A(x)}$و${\displaystyle B(x)}$، أين${\displaystyle x}$مجاني في كليهما، الصيغة التي يمثلها الجدول هي شيء من الشكل${\displaystyle \forall x.(...A(x)...B(x)...)}$تشير هذه الصيغة إلى أن${\displaystyle (...A(x)...B(x)...)}$هذا صحيح لأي قيمة من${\displaystyle x}$لكن هذا لا يعني بالضرورة${\displaystyle (...A(t)...A(t')...)}$لمصطلحين مختلفين${\displaystyle t}$و${\displaystyle t'}$حيث أن هذين المصطلحين قد يأخذان قيماً مختلفة بشكل عام. وهذا يعني أن${\displaystyle x}$لا يمكن استبدالها بمصطلحين مختلفين في${\displaystyle A(x)}$و${\displaystyle B(x)}$.
• تُعتبر المتغيرات الحرة في الصيغة المستخدمة للتحقق من صحتها متغيرات كمية عالمية. مع ذلك، لا يمكن ترك هذه المتغيرات حرة عند إنشاء جدول بيانات، لأن قواعد الجدول تعمل على عكس الصيغة، لكنها مع ذلك تعامل المتغيرات الحرة على أنها متغيرات كمية عالمية. على سبيل المثال،${\displaystyle P(x)\to P(c)}$غير صالح (ليس صحيحًا في النموذج حيث${\displaystyle D=\{1,2\},P(1)=\bot ,P(2)=\top ,c=1}$والتفسير حيث${\displaystyle x=2}$). بالتالي،${\displaystyle \{P(x),\neg P(c)\}}$قابلة للتحقيق (يتم تحقيقها بنفس النموذج والتفسير). ومع ذلك، يمكن إنشاء جدول مغلق باستخدام${\displaystyle P(x)}$و${\displaystyle \neg P(c)}$واستبدالها${\displaystyle x}$مع${\displaystyle c}$سيؤدي ذلك إلى إنشاء إغلاق. الإجراء الصحيح هو أولاً جعل المحددات الكمية الشاملة صريحة، وبالتالي إنشاء${\displaystyle \forall x.(P(x)\to P(c))}$.

الخياران التاليان صحيحان أيضاً.

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

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

يتمثل أحد حلول هذه المشكلة في التأجيل : حيث لا يُطبَّق أي استبدال حتى يتم العثور على استبدال يُغلق جميع الفروع في آنٍ واحد. باستخدام هذا الأسلوب، يمكن دائمًا إيجاد برهان لمجموعة غير قابلة للإرضاء من خلال سياسة مناسبة لتطبيق القواعد الأخرى. مع ذلك، تتطلب هذه الطريقة الاحتفاظ بالجدول بأكمله في الذاكرة: فالطريقة العامة تُغلق الفروع، والتي يمكن تجاهلها بعد ذلك، بينما لا يُغلق هذا الأسلوب أي فرع حتى النهاية.

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

يعتمد حجم شجرة البحث على عدد الجداول الفرعية (الأبناء) التي يمكن توليدها من جدول رئيسي (أصلي) معين. وبالتالي، فإن تقليل عدد هذه الجداول يقلل من حجم البحث المطلوب.

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

تمنع بعض طرق تقليل البحث إنشاء بعض الجداول، وذلك لأن الجدول المغلق لا يزال من الممكن إيجاده بتوسيع الجداول الأخرى. تُسمى هذه القيود بالقيود العامة. كمثال على قيد عام، يمكن استخدام قاعدة تحدد أيًّا من الفروع المفتوحة سيتم توسيعه. بالتالي، إذا كان للجدول، على سبيل المثال، فرعان غير مغلقين، فإن القاعدة تحدد أيًّا منهما سيتم توسيعه، مما يمنع توسيع الفرع الثاني. يقلل هذا القيد من مساحة البحث لأن أحد الخيارات الممكنة أصبح ممنوعًا؛ ومع ذلك، لا تتأثر اكتمالية البحث، حيث سيتم توسيع الفرع الثاني إذا تم إغلاق الفرع الأول في النهاية. على سبيل المثال، جدول ذو جذر${\displaystyle \neg a\land \neg b}$، طفل${\displaystyle a\lor b}$وورقتان${\displaystyle a}$و${\displaystyle b}$يمكن إغلاقها بطريقتين: تطبيق${\displaystyle (\land )}$أولًا لـ${\displaystyle a}$ثم إلى${\displaystyle b}$أو العكس. من الواضح أنه لا داعي لاتباع كلا الاحتمالين؛ يمكن للمرء أن ينظر فقط في الحالة التي يكون فيها${\displaystyle (\land )}$يتم تطبيقه أولاً على${\displaystyle a}$وتجاهل الحالة التي يتم فيها تطبيقها لأول مرة على${\displaystyle b}$هذا قيد عالمي لأن ما يسمح بتجاهل هذا التوسع الثاني هو وجود الجدول الآخر، حيث يتم تطبيق التوسع على${\displaystyle a}$أولاً و${\displaystyle b}$بعد ذلك.

الاتصال هو شرط في جدول البيانات يمنع توسيع فرع باستخدام عبارات لا علاقة لها بالقيم الحرفية الموجودة بالفعل في الفرع. يمكن تعريف الاتصال بطريقتين:

روابط قوية

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

اتصال ضعيف

السماح باستخدام العبارات التي تحتوي على قيمة حرفية تتحد مع نفي قيمة حرفية أخرى في الفرع

ينطبق كلا الشرطين فقط على الفروع التي لا تقتصر على الجذر. يسمح التعريف الثاني باستخدام عبارة تحتوي على حرف يتحد مع نفي حرف في الفرع، بينما يقيد التعريف الأول هذا الحرف فقط ليكون في ورقة الفرع الحالي.

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

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

يمكن ملاحظة ذلك في المثال (الافتراضي) التالي. اللوحة المكونة من سلسلة${\displaystyle true-a}$بالنسبة لمجموعة البنود${\displaystyle \{a,\neg a\lor b,\neg c\lor d,\neg b\}}$يمكن توسيعها بشكل عام باستخدام كل من بنود الإدخال الأربعة، لكن الاتصال لا يسمح إلا بالتوسيع الذي يستخدم${\displaystyle \neg a\lor b}$هذا يعني أن شجرة الجداول تحتوي على أربع أوراق في الوضع العام، ولكنها تحتوي على ورقة واحدة فقط في حالة فرض الاتصال. وهذا يعني أن الاتصال يترك جدولًا واحدًا فقط لمحاولة توسيعه، بدلًا من الجداول الأربعة التي يجب مراعاتها في الوضع العام. وعلى الرغم من هذا النقص في الخيارات، فإن نظرية الاكتمال تشير إلى أنه يمكن إيجاد جدول مغلق إذا كانت المجموعة غير قابلة للإرضاء.

تؤدي شروط الاتصال، عند تطبيقها على الحالة الافتراضية (الجملية)، إلى جعل الحساب الناتج غير متصل. على سبيل المثال،${\displaystyle \{a,b,\neg b\}}$غير مُرضٍ، ولكن تطبيق${\displaystyle (C)}$ل${\displaystyle a}$يُولّد السلسلة${\displaystyle true-a}$وهي مجموعة غير مغلقة، ولا يمكن تطبيق أي قاعدة توسيع أخرى عليها دون الإخلال بشرطي الاتصال القوي أو الضعيف. في حالة الاتصال الضعيف، يتحقق التقارب بشرط أن يكون الشرط المستخدم لتوسيع الجذر ذا صلة بعدم إمكانية الإرضاء، أي أنه يقع ضمن مجموعة فرعية غير قابلة للإرضاء بشكل أدنى من مجموعة الشروط. لسوء الحظ، تُعدّ مشكلة التحقق مما إذا كان الشرط يستوفي هذا الشرط مشكلة معقدة بحد ذاتها. على الرغم من عدم التقارب، يمكن إيجاد جدول مغلق باستخدام البحث، كما هو موضح في قسم "البحث عن جدول مغلق" أعلاه. في حين أن البحث ضروري، فإن الاتصال يقلل من خيارات التوسيع الممكنة، مما يجعل البحث أكثر كفاءة.

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

لكن خطوات التوسع غير المسموح بها هذه عديمة الفائدة. إذا${\displaystyle B}$هو فرع يحتوي على حرفي${\displaystyle L}$، و${\displaystyle C}$إذا كانت جملة يخالف توسيعها قواعد الانتظام،${\displaystyle C}$يتضمن${\displaystyle L}$لإغلاق الجدول، يجب توسيع وإغلاق الفرع الذي، من بين أمور أخرى،${\displaystyle B-L}$، أين${\displaystyle L}$يحدث ذلك مرتين. ومع ذلك، فإن الصيغ في هذا الفرع هي نفسها تمامًا صيغ الفرع الآخر.${\displaystyle B}$بمفرده. ونتيجة لذلك، فإن نفس خطوات التوسع التي تغلق${\displaystyle B-L}$قريب أيضًا${\displaystyle B}$وهذا يعني التوسع${\displaystyle C}$كان ذلك غير ضروري؛ علاوة على ذلك، إذا${\displaystyle C}$احتوى على متغيرات حرفية أخرى، وأدى توسيعه إلى ظهور أوراق أخرى تحتاج إلى إغلاق. في الحالة المنطقية، يكون التوسيع اللازم لإغلاق هذه الأوراق عديم الفائدة تمامًا؛ أما في حالة الرتبة الأولى، فقد يؤثر فقط على بقية الجدول بسبب بعض عمليات التوحيد؛ ومع ذلك، يمكن دمج هذه العمليات مع عمليات الاستبدال المستخدمة لإغلاق بقية الجدول.

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

على سبيل المثال، في S5 كل صيغة${\displaystyle \Box A}$ما يصدق في عالم ما يصدق أيضاً في جميع العوالم التي يمكن الوصول إليها (أي في جميع العوالم التي يمكن الوصول إليها).${\displaystyle A}$و${\displaystyle \Box A}$(صحيح). لذلك، عند تطبيق${\displaystyle {\frac {\neg \Box B}{\neg B}}}$، والتي تنطبق نتيجتها في عالم مختلف، يتم حذف جميع الصيغ من الفرع، ولكن يمكن الاحتفاظ بجميع الصيغ.${\displaystyle \Box A}$كما هو الحال في العالم الجديد أيضاً. وللحفاظ على الشمولية، تُضاف الصيغ المحذوفة إلى جميع الفروع الأخرى التي لا تزال تشير إلى العالم القديم.

تتمثل آلية أخرى لضمان التفاعل الصحيح بين الصيغ التي تشير إلى عوالم مختلفة في التحول من الصيغ إلى الصيغ المُعَلَّمة: بدلاً من كتابة${\displaystyle A}$يكتب المرء${\displaystyle w:A}$لتوضيح ذلك${\displaystyle A}$يحتلّ مكانةً عالميةً${\displaystyle w}$.

تُكيَّف جميع قواعد توسيع القضايا مع هذا المتغير من خلال النص على أنها جميعًا تشير إلى صيغ تحمل نفس التسمية العالمية. على سبيل المثال،${\displaystyle w:A\land B}$يُنشئ عقدتين مُصنفتين بـ${\displaystyle w:A}$و${\displaystyle w:B}$لا يُغلق الفرع إلا إذا احتوى على حرفين متقابلين لنفس العالم، مثل${\displaystyle w:a}$و${\displaystyle w:\neg a}$لا يتم إنشاء إغلاق إذا كانت تسميات العالمين مختلفة، كما هو الحال في${\displaystyle w:a}$و${\displaystyle w':\neg a}$.

قد يكون لقاعدة توسيع الحالة المشروطة نتيجة تشير إلى عوالم مختلفة. على سبيل المثال، قاعدة لـ${\displaystyle \neg \Box A}$ستُكتب على النحو التالي

${\displaystyle {\frac {w:\neg \Box A}{w':\neg A}}}$

يشير الشرط المسبق والنتيجة المترتبة على هذه القاعدة إلى العوالم${\displaystyle w}$و${\displaystyle w'}$على التوالي. تستخدم الحسابات المختلفة طرقًا مختلفة لتتبع إمكانية الوصول إلى العوالم المستخدمة كعلامات. يتضمن بعضها صيغًا زائفة مثل${\displaystyle wRw'}$للدلالة على ذلك${\displaystyle w'}$يمكن الوصول إليه من${\displaystyle w}$يستخدم البعض الآخر سلاسل من الأعداد الصحيحة كعلامات للعالم، ويمثل هذا الترميز ضمنيًا علاقة إمكانية الوصول (على سبيل المثال،${\displaystyle (1,4,2,3)}$يمكن الوصول إليه من${\displaystyle (1,4,2)}$.)

يمكن التغلب على مشكلة التفاعل بين الصيغ المستخدمة في عوالم مختلفة باستخدام جداول تصنيف المجموعات. هذه الجداول عبارة عن أشجار تُصنّف عُقدها بمجموعات من الصيغ؛ وتوضح قواعد التوسع كيفية ربط عُقد جديدة بورقة، بناءً على تصنيف الورقة فقط (وليس على تصنيف العُقد الأخرى في الفرع).

تُستخدم جداول المنطق الموجه للتحقق من إمكانية تحقيق مجموعة من الصيغ الموجهية في منطق موجه معين. بالنظر إلى مجموعة من الصيغ...${\displaystyle S}$يتحققون من وجود نموذج${\displaystyle M}$وعالم${\displaystyle w}$بحيث${\displaystyle M,w\models S}$.

تعتمد قواعد التوسع على المنطق الموجه المستخدم. ويمكن الحصول على نظام جدولي للمنطق الموجه الأساسي K بإضافة القاعدة التالية إلى قواعد الجدول الافتراضي:

${\displaystyle (K){\frac {\Box A_{1};\ldots$ ;\Box A_{n};\neg \Box B}{A_{1};\ldots ;A_{n};\neg B}}}

وبشكل بديهي، فإن الشرط المسبق لهذه القاعدة يعبر عن صحة جميع الصيغ.${\displaystyle A_{1},\ldots ,A_{n}}$في جميع العوالم المتاحة، وحقيقة${\displaystyle \neg B}$في بعض العوالم التي يمكن الوصول إليها. نتيجة هذه القاعدة هي صيغة يجب أن تكون صحيحة في أحد تلك العوالم حيث${\displaystyle \neg B}$هذا صحيح.

وبشكل أكثر دقة، تتحقق طرق الجداول النموذجية من وجود نموذج${\displaystyle M}$وعالم${\displaystyle w}$التي تجعل مجموعة الصيغ صحيحة. إذا${\displaystyle \Box A_{1};\ldots$ ;\Box A_{n};\neg \Box B} صحيحان في${\displaystyle w}$لا بد أن يكون هناك عالم${\displaystyle w'}$يمكن الوصول إليه من${\displaystyle w}$وهذا يجعل${\displaystyle A_{1};\ldots ;A_{n};\neg B}$صحيح. وبالتالي، فإن هذه القاعدة تعني اشتقاق مجموعة من الصيغ التي يجب استيفاؤها في مثل هذه الحالة.${\displaystyle w'}$.

بينما الشروط المسبقة${\displaystyle \Box A_{1};\ldots$ يُفترض أن الشرطين ;\Box A_{n};\neg \Box B} مُحققان بواسطة${\displaystyle M,w}$، والعواقب${\displaystyle A_{1};\ldots ;A_{n};\neg B}$يُفترض استيفاء الشروط في${\displaystyle M,w'}$نفس النموذج ولكن ربما عوالم مختلفة. لا تُسجّل الجداول المُصنّفة حسب المجموعات العالم الذي يُفترض فيه صحة كل صيغة بشكل صريح: قد تُشير عقدتان إلى نفس العالم أو لا. ومع ذلك، تُفترض صحة الصيغ التي تُصنّف أي عقدة معينة في نفس العالم.

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

والجدير بالذكر،${\displaystyle (K)}$لا يمتد ذلك بشكل مباشر إلى الصيغ المتعددة المنفية داخل المربعات كما في${\displaystyle \Box A_{1};\ldots$ ;\Box A_{n};\neg \Box B_{1};\neg \Box B_{2}} : طالما يوجد عالم يمكن الوصول إليه حيث${\displaystyle B_{1}}$خاطئ، وهو واحد من${\displaystyle B_{2}}$هذا غير صحيح، فهذان العالمان ليسا بالضرورة متطابقين.

على عكس القواعد الافتراضية،${\displaystyle (K)}$تُحدد الشروط جميع شروطها المسبقة. على سبيل المثال، لا يمكن تطبيقها على عقدة مُصنفة بواسطة${\displaystyle a;\Box b;\Box (b\to c);\neg \Box c}$بينما هذه المجموعة غير متسقة، ويمكن إثبات ذلك بسهولة بتطبيق${\displaystyle (K)}$لا يمكن تطبيق هذه القاعدة بسبب الصيغة${\displaystyle a}$وهذا لا علاقة له حتى بالتناقض. ويمكن إزالة هذه الصيغ بموجب القاعدة التالية:

${\displaystyle (\theta ){\frac {A_{1};\ldots ;A_{n};B_{1};\ldots ;B_{m}}{A_{1};\ldots ;A_{n}}}}$

إن إضافة هذه القاعدة (قاعدة التخفيف) تجعل الحساب الناتج غير متقارب: قد يكون من المستحيل إغلاق جدول لمجموعة غير متسقة، حتى لو كان هناك جدول مغلق لنفس المجموعة.

قاعدة${\displaystyle (\theta )}$هي غير حتمية: يمكن اختيار مجموعة الصيغ المراد حذفها (أو الاحتفاظ بها) بشكل عشوائي؛ وهذا يخلق مشكلة اختيار مجموعة صيغ للتخلص منها بحيث لا تكون كبيرة جدًا بحيث تجعل المجموعة الناتجة قابلة للتحقيق، ولا صغيرة جدًا بحيث تجعل قواعد التوسع اللازمة غير قابلة للتطبيق. وجود عدد كبير من الخيارات الممكنة يجعل مشكلة البحث عن جدول مغلق أكثر صعوبة.

يمكن تجنب هذا الغموض عن طريق تقييد استخدام${\displaystyle (\theta )}$بحيث يتم تطبيقها فقط قبل قاعدة توسيع مشروطة، وبحيث تزيل فقط الصيغ التي تجعل تلك القاعدة الأخرى غير قابلة للتطبيق. يمكن أيضًا صياغة هذا الشرط بدمج القاعدتين في قاعدة واحدة. تُنتج القاعدة الناتجة نفس نتيجة القاعدة القديمة، ولكنها تتجاهل ضمنيًا جميع الصيغ التي جعلت القاعدة القديمة غير قابلة للتطبيق. هذه آلية للإزالة${\displaystyle (\theta )}$وقد ثبت أنها تحافظ على الاكتمال للعديد من المنطق الموجه.

تُعبّر البديهية T عن انعكاسية علاقة الوصول: كل عالم يمكن الوصول إليه من ذاته. وقاعدة توسيع الجدول المقابلة هي:

${\displaystyle (T){\frac {A_{1};\ldots ;A_{n};\Box B}{A_{1};\ldots ;A_{n};\Box B;B}}}$

تربط هذه القاعدة الشروط في نفس العالم: إذا${\displaystyle \Box B}$صحيح في عالم، عن طريق الانعكاسية${\displaystyle B}$وينطبق هذا أيضاً في العالم نفسه . هذه القاعدة ثابتة وليست تفاعلية، حيث يشير كل من شرطها المسبق ونتيجتها إلى العالم نفسه.

تنسخ هذه القاعدة${\displaystyle \Box B}$من الشرط المسبق إلى النتيجة، على الرغم من استخدام هذه الصيغة لتوليد${\displaystyle B}$هذا صحيح، لأن العالم المعتبر هو نفسه، لذا${\displaystyle \Box B}$وينطبق الأمر نفسه هناك. هذا "النسخ" ضروري في بعض الحالات. على سبيل المثال، من الضروري إثبات عدم اتساق ${\displaystyle \Box (a\land \neg \Box a)}$القواعد الوحيدة المطبقة هي القواعد المنظمة${\displaystyle (T),(\land ),(\theta ),(K)}$، والتي يُمنع المرء من الوصول إليها إذا${\displaystyle \Box a}$لم يتم نسخها.

ثمة طريقة أخرى للتعامل مع الصيغ التي تنطبق على العوالم البديلة، وهي إنشاء جدول بيانات مختلف لكل عالم جديد يتم إدخاله في الجدول. على سبيل المثال،${\displaystyle \neg \Box A}$يشير ذلك إلى أن${\displaystyle A}$هذا غير صحيح في عالم متاح، لذلك يبدأ المرء لوحة جديدة متجذرة في${\displaystyle \neg A}$يتم ربط هذا الجدول الجديد بعقدة الجدول الأصلي حيث طُبقت قاعدة التوسيع؛ ويؤدي إغلاق هذا الجدول مباشرةً إلى إغلاق جميع الفروع التي تقع عندها تلك العقدة، بغض النظر عما إذا كانت العقدة نفسها مرتبطة بجداول مساعدة أخرى. قواعد التوسيع للجداول المساعدة هي نفسها قواعد التوسيع للجدول الأصلي؛ لذلك، يمكن أن يحتوي الجدول المساعد بدوره على جداول مساعدة (فرعية) أخرى.

تُثبت الجداول النموذجية المذكورة أعلاه اتساق مجموعة من الصيغ، ويمكن استخدامها لحل مشكلة الاستدلال المنطقي المحلي . وتتمثل هذه المشكلة في تحديد ما إذا كان، بالنسبة لكل نموذج${\displaystyle M}$، لو${\displaystyle A}$هذا صحيح في عالم${\displaystyle w}$، ثم${\displaystyle B}$وينطبق هذا أيضاً في العالم نفسه. وهذا يشبه التحقق مما إذا كان${\displaystyle B}$هذا صحيح في عالم نموذجي، بافتراض أن${\displaystyle A}$وينطبق هذا أيضاً في نفس العالم وفي نفس النموذج.

تتمثل إحدى المشكلات ذات الصلة في مشكلة العواقب العالمية، حيث يُفترض أن الصيغة (أو مجموعة الصيغ)${\displaystyle G}$صحيح في جميع العوالم الممكنة للنموذج. تكمن المشكلة في التحقق مما إذا كان هذا صحيحًا في جميع النماذج${\displaystyle M}$أين${\displaystyle G}$هذا صحيح في جميع العوالم،${\displaystyle B}$وينطبق هذا أيضاً على جميع العوالم.

تختلف الافتراضات المحلية والعالمية في النماذج التي تكون فيها الصيغة المفترضة صحيحة في بعض العوالم ولكنها غير صحيحة في عوالم أخرى. على سبيل المثال،${\displaystyle \{P,\neg \Box (P\land Q)\}}$يستلزم${\displaystyle \neg \Box Q}$عالميًا وليس محليًا. لا ينطبق الاستلزام المحلي في نموذج يتكون من عالمين.${\displaystyle P}$و${\displaystyle \neg P,Q}$صحيح، على التوالي، وحيث يمكن الوصول إلى الثاني من الأول؛ في العالم الأول، تكون الافتراضات صحيحة ولكن${\displaystyle \neg \Box Q}$هذا غير صحيح. هذا المثال المضاد يعمل لأن${\displaystyle P}$يمكن افتراض صحة هذا الافتراض في عالم ما وخطئه في عالم آخر. أما إذا اعتُبر الافتراض نفسه عالميًا،${\displaystyle \neg P}$غير مسموح به في أي عالم من عوالم النموذج.

يمكن دمج هاتين المشكلتين، بحيث يمكن للمرء التحقق مما إذا${\displaystyle B}$وهي نتيجة محلية لـ${\displaystyle A}$في ظل الافتراض العالمي${\displaystyle G}$يمكن لحسابات الجداول التعامل مع الافتراض العالمي من خلال قاعدة تسمح بإضافته إلى كل عقدة، بغض النظر عن العالم الذي تشير إليه.

عند كتابة قواعد توسيع الجداول، غالبًا ما يتم الإشارة إلى الصيغ باستخدام اصطلاح معين، بحيث يُعتبر α دائمًا على سبيل المثال${\displaystyle \alpha _{1}\land \alpha _{2}}$يوضح الجدول التالي الرموز المستخدمة في الصيغ في المنطق الافتراضي، والمنطق من الدرجة الأولى، والمنطق الموجه.

الترميز	الصيغ
α	${\displaystyle \alpha _{1}\land \alpha _{2}}$	${\displaystyle \neg ({\overline {\alpha _{1}}}\lor {\overline {\alpha _{2}}})}$	${\displaystyle \neg (\alpha _{1}\to {\overline {\alpha _{2}}})}$
β	${\displaystyle \beta _{1}\lor \beta _{2}}$	${\displaystyle {\overline {\beta _{1}}}\to \beta _{2}}$	${\displaystyle \neg ({\overline {\beta _{1}}}\land {\overline {\beta _{2}}})}$
γ	${\displaystyle \forall x\gamma _{1}(x)}$	${\displaystyle \neg \exists x{\overline {\gamma _{1}(x)}}}$
دلتا	${\displaystyle \exists x\delta _{1}(x)}$	${\displaystyle \neg \forall x{\overline {\delta _{1}(x)}}}$
π	${\displaystyle \Diamond \pi _{1}}$	${\displaystyle \neg \Box {\overline {\pi _{1}}}}$
ν	${\displaystyle \Box \nu _{1}}$	${\displaystyle \neg \Diamond {\overline {\nu _{1}}}}$

يُعتبر كل تصنيف في العمود الأول بمثابة إحدى الصيغتين في الأعمدة الأخرى. صيغة مُسطّرة مثل${\displaystyle {\overline {\alpha _{1}}}}$يشير إلى أن${\displaystyle \alpha _{1}}$هو نفي أي صيغة تظهر مكانه، بحيث يكون على سبيل المثال في الصيغة${\displaystyle \neg (a\lor b)}$الصيغة الفرعية${\displaystyle \alpha _{1}}$هو نفي لـ أ .

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

${\displaystyle (\alpha ){\frac {\alpha }{\begin{array}{c}\alpha _{1}\\\alpha _{2}\end{array}}}}$