القرار (المنطق)

قاعدة الاستدلال في منطق القضايا هي قاعدة استدلال صحيحة واحدة تُنتج عبارة جديدة مُستنتجة من عبارتين تحتويان على متغيرات مُكملة. المتغير هو إما متغير قضية أو نفي لمتغير قضية. يُقال إن متغيرين مُكملان إذا كان أحدهما نفيًا للآخر (فيما يلي، ${\displaystyle \lnot c}$يُعتبر مكملاً لـ${\displaystyle c}$تحتوي الجملة الناتجة على جميع القيم الحرفية التي لا تحتوي على مكملات. رسميًا:

${\displaystyle {\frac {a_{1}\lor a_{2}\lor \cdots \lor c,\quad b_{1}\lor b_{2}\lor \cdots \lor \neg c}{a_{1}\lor a_{2}\lor \cdots \lor b_{1}\lor b_{2}\lor \cdots }}}$

أين

الجميع${\displaystyle a_{i}}$،${\displaystyle b_{i}}$، و${\displaystyle c}$هي أحرف حرفية،

يرمز الخط الفاصل إلى " يستلزم ".

يمكن كتابة ما سبق أيضًا على النحو التالي:

${\displaystyle {\frac {(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow c,\quad c\rightarrow (b_{1}\lor b_{2}\lor \cdots )}{(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow (b_{1}\lor b_{2}\lor \cdots )}}}$

أو بشكل تخطيطي كما يلي:

${\displaystyle {\frac {\Gamma _{1}\cup \left\{\ell \right\}\,\,\,\,\Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}{\Gamma _{1}\cup \Gamma _{2}}}|\ell |}$

لدينا المصطلحات التالية:

• البنود${\displaystyle \Gamma _{1}\cup \left\{\ell \right\}}$ و${\displaystyle \Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}$هي مقدمات الاستدلال
• ${\displaystyle \Gamma _{1}\cup \Gamma _{2}}$(مُحَلِّل المقدمات) هو نتيجتها.
• المعنى الحرفي${\displaystyle \ell }$هو الحرف المحلول من اليسار،
• المعنى الحرفي${\displaystyle {\overline {\ell }}}$هو الحرف الصحيح المُحلَّل،
• ${\displaystyle |\ell |}$هي الذرة أو المحور المحدد.

The clause produced by the resolution rule is called the resolvent of the two input clauses. It is the principle of consensus applied to clauses rather than terms.^[3]

When the two clauses contain more than one pair of complementary literals, the resolution rule can be applied (independently) for each such pair; however, the result is always a tautology.

Modus ponens can be seen as a special case of resolution (of a one-literal clause and a two-literal clause).

${\displaystyle {\frac {p\rightarrow q,\quad p}{q}}}$

is equivalent to

${\displaystyle {\frac {\lnot p\lor q,\quad p}{q}}}$

When coupled with a complete search algorithm, the resolution rule yields a sound and complete algorithm for deciding the satisfiability of a propositional formula, and, by extension, the validity of a sentence under a set of axioms.

This resolution technique uses proof by contradiction and is based on the fact that any sentence in propositional logic can be transformed into an equivalent sentence in conjunctive normal form.^[4] The steps are as follows.

• All sentences in the knowledge base and the negation of the sentence to be proved (the conjecture) are conjunctively connected.
• The resulting sentence is transformed into a conjunctive normal form with the conjuncts viewed as elements in a set, S, of clauses.^[4]
  • For example, ${\displaystyle (A_{1}\lor A_{2})\land (B_{1}\lor B_{2}\lor B_{3})\land (C_{1})}$ gives rise to the set ${\displaystyle S=\{A_{1}\lor A_{2},B_{1}\lor B_{2}\lor B_{3},C_{1}\}}$.
• The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the clause contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set S, it is added to S, and is considered for further resolution inferences.
• If after applying a resolution rule the empty clause is derived, the original formula is unsatisfiable (or contradictory), and hence it can be concluded that the initial conjecture follows from the axioms.
• If, on the other hand, the empty clause cannot be derived, and the resolution rule cannot be applied to derive any more new clauses, the conjecture is not a theorem of the original knowledge base.

One instance of this algorithm is the original Davis–Putnam algorithm that was later refined into the DPLL algorithm that removed the need for explicit representation of the resolvents.

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

البنود${\displaystyle P(x),Q(x)}$و${\displaystyle \neg P(b)}$يمكن تطبيق هذه القاعدة مع${\displaystyle [b/x]}$كعامل موحد.

هنا x متغير و b ثابت.

${\displaystyle {\frac {P(x),Q(x)\,\,\,\,\neg P(b)}{Q(b)}}[b/x]}$

هنا نرى ذلك

• البنود${\displaystyle P(x),Q(x)}$ و${\displaystyle \neg P(b)}$هي مقدمات الاستدلال
• ${\displaystyle Q(b)}$(مُحَلِّل المقدمات) هو نتيجتها.
• المعنى الحرفي${\displaystyle P(x)}$هو الحرف المحلول من اليسار،
• المعنى الحرفي${\displaystyle \neg P(b)}$هو الحرف الصحيح المُحلَّل،
• ${\displaystyle P}$هي الذرة أو المحور المحدد.
• ${\displaystyle [b/x]}$هو أكثر موحد عام للحرفيات المحلولة.

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

لفهم كيفية عمل الاستدلال المنطقي، انظر إلى مثال القياس المنطقي التالي لمنطق المصطلحات :

جميع اليونانيين أوروبيون.

هوميروس يوناني.

لذلك، فإن هوميروس أوروبي.

أو بشكل أعم:

${\displaystyle \forall xP(x)\Rightarrow Q(x)}$

${\displaystyle P(a)}$

لذلك،${\displaystyle Q(a)}$

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

${\displaystyle \neg P(x)\vee Q(x)}$

${\displaystyle P(a)}$

لذلك،${\displaystyle Q(a)}$

إذن، السؤال هو: كيف تستنتج تقنية الاستدلال العبارة الأخيرة من العبارتين الأوليين؟ القاعدة بسيطة:

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

لتطبيق هذه القاعدة على المثال أعلاه، نجد أن المسند P يظهر في صورة منفية

¬ P ( X )

في الجملة الأولى، وبصيغة غير منفية

P ( أ )

في العبارة الثانية، X متغير غير مقيد، بينما a قيمة مقيدة (حد). توحيد الاثنين ينتج عنه الاستبدال

X ↦ a

يؤدي تجاهل المسندات الموحدة، وتطبيق هذا الاستبدال على المسندات المتبقية ( Q ( X ) فقط في هذه الحالة)، إلى النتيجة التالية:

س ( أ )

كمثال آخر، انظر إلى الشكل القياسي

جميع الكريتيين هم من سكان الجزر.

جميع سكان الجزيرة كاذبون.

لذلك فإن جميع الكريتيين كاذبون.

أو بشكل أعم،

∀ X P ( X ) → Q ( X )

∀ X Q ( X ) → R ( X )

لذلك، لكل X، P ( X ) → R ( X )

في صيغة CNF، تصبح المقدمات كالتالي:

¬ P ( X ) ∨ Q ( X )

¬ Q ( Y ) ∨ R ( Y )

(تمت إعادة تسمية المتغير في الجملة الثانية لتوضيح أن المتغيرات في الجمل المختلفة متميزة.)

الآن، بتوحيد Q ( X ) في العبارة الأولى مع ¬Q ( Y ) في العبارة الثانية، يصبح X و Y متغيرين متطابقين. وبالتعويض بهذا في العبارات المتبقية ودمجها، نحصل على النتيجة التالية:

¬ P ( X ) ∨ R ( X )

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

مثال على مجموعة عبارات غير قابلة للإرضاء والتي تتطلب تحليلًا إلى عوامل لاستنتاج العبارة الفارغة هو:

${\displaystyle {\begin{array}{rlcl}(1):&P(u)&\lor &P(f(u))\\(2):&\lnot P(v)&\lor &P(f(w))\\(3):&\lnot P(x)&\lor &\lnot P(f(x))\\\end{array}}}$

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

${\displaystyle {\begin{array}{rll}(4):&P(u)\lor P(f(w))&{\text{by resolving (1) and (2), with }}v=f(u)\\(5):&P(f(w))&{\text{by factoring (4), with }}u=f(w)\\(6):&\lnot P(f(f(w')))&{\text{by resolving (5) and (3), with }}w=w',x=f(w')\\(7):&{\text{false}}&{\text{by resolving (5) and (6), with }}w=f(w')\\\end{array}}}$

فيما يخص منطق القضايا، يستخدم كل من موراي ^{[ 9 ] : 18} ومانا ووالدينجر ^{[ 10 ] : 98} القاعدة التالية

${\displaystyle {\begin{array}{c}F[p]\;\;\;\;\;\;\;\;\;\;G[p]\\\hline F[{\textit {true}}]\lor G[{\textit {false}}]\\\end{array}}}$،

أين${\displaystyle p}$يرمز إلى صيغة اختيارية. هنا${\displaystyle F[p]}$و${\displaystyle G[p]}$تشير إلى الصيغ التي تحتوي على${\displaystyle p}$كصيغة فرعية.${\displaystyle F[{\textit {true}}]}$يتم بناؤها عن طريق استبدال كل ظهور لـ${\displaystyle p}$في${\displaystyle F[p]}$بواسطة${\displaystyle {\textit {true}}}$. بصورة مماثلة،${\displaystyle G[{\textit {false}}]}$يتم بناؤها عن طريق استبدال كل ظهور لـ${\displaystyle p}$في${\displaystyle G[p]}$بواسطة${\displaystyle {\textit {false}}}$المُذيب${\displaystyle F[{\textit {true}}]\lor G[{\textit {false}}]}$يهدف إلى التبسيط باستخدام قواعد مثل${\displaystyle q\land {\textit {true}}\implies q}$إلخ. ولمنع توليد دوال حل تافهة وغير مفيدة، لا تُطبق القاعدة إلا عندما${\displaystyle p}$يحتوي على حالة واحدة على الأقل "سلبية" وحالة واحدة على الأقل "إيجابية" ^{[ 14 ]} في${\displaystyle F}$و${\displaystyle G}$على التوالي. وقد بيّن موراي أن هذه القاعدة كاملة إذا ما أُضيفت إليها قواعد تحويل منطقية مناسبة. ^{[ 10 ] : 103}

يستخدم تراوغوت قاعدة يمكن التعبير عنها بشكل مشابه على النحو التالي

${\displaystyle {\begin{array}{c}F[p^{+},p^{-}]\;\;\;\;\;\;\;\;G[p]\\\hline F[G[{\textit {true}}],\lnot G[{\textit {false}}]]\\\end{array}}}$،

حيث أسس${\displaystyle p}$يشير ذلك إلى قطبية حدوثه. بينما${\displaystyle G[{\textit {true}}]}$و${\displaystyle G[{\textit {false}}]}$يتم بناؤها كما في السابق، الصيغة${\displaystyle F[G[{\textit {true}}],\lnot G[{\textit {false}}]]}$يتم الحصول عليها عن طريق استبدال كل ظهور موجب لـ${\displaystyle p}$في${\displaystyle F}$مع${\displaystyle G[{\textit {true}}]}$وكل حدث سلبي مع${\displaystyle G[{\textit {false}}]}$على غرار منهج موراي، تُطبَّق تحويلات تبسيطية مناسبة على المُحلِّل. وقد أثبت تراوغوت اكتمال قاعدته، شريطة${\displaystyle \land ,\lor ,\rightarrow ,\lnot }$هي الروابط الوحيدة المستخدمة في الصيغ. ^{[ 12 ] : 398-400}

يُعدّ مُحلِّل تراوغوت أقوى من مُحلِّل موراي. ^{[ 12 ] : 395} علاوة على ذلك، فهو لا يُدخل روابط ثنائية جديدة، وبالتالي يتجنّب الميل نحو الصيغة الشرطية في الاستدلال المتكرر. مع ذلك، قد تطول الصيغ عندما يكون مُحلِّل تراوغوت صغيرًا.${\displaystyle p}$يتم استبدالها عدة مرات بواحدة أكبر${\displaystyle G[{\textit {true}}]}$و/أو${\displaystyle G[{\textit {false}}]}$[ ^{12 ] : 398​}

على سبيل المثال، انطلاقاً من الافتراضات التي يقدمها المستخدم

${\displaystyle {\begin{array}{rccc}(1):&a&\rightarrow &b\land c\\(2):&c&\rightarrow &d\\(3):&b\land d&\rightarrow &e\\(4):&\lnot (a&\rightarrow &e)\\\end{array}}}$

يمكن استخدام قاعدة موراي على النحو التالي لاستنتاج التناقض: ^{[ 15 ]}

${\displaystyle {\begin{array}{rrclccl}(5):&({\textit {true}}\rightarrow d)&\lor &(a\rightarrow b\land {\textit {false}})&\implies &d\lor \lnot a&{\mbox{from (2) and (1), with }}p=c\\(6):&(b\land {\textit {true}}\rightarrow e)&\lor &({\textit {false}}\lor \lnot a)&\implies &(b\rightarrow e)\lor \lnot a&{\mbox{from (3) and (5), with }}p=d\\(7):&(({\textit {true}}\rightarrow e)\lor \lnot a)&\lor &(a\rightarrow {\textit {false}}\land c)&\implies &e\lor \lnot a\lor \lnot a&{\mbox{from (6) and (1), with }}p=b\\(8):&(e\lor \lnot {\textit {true}}\lor \lnot {\textit {true}})&\lor &\lnot ({\textit {false}}\rightarrow e)&\implies &e&{\mbox{from (7) and (4), with }}p=a\\(9):&\lnot (a\rightarrow {\textit {true}})&\lor &{\textit {false}}&\implies &{\textit {false}}&{\mbox{from (4) and (8), with }}p=e\\\end{array}}}$

وللغرض نفسه، يمكن استخدام قاعدة تراوغوت على النحو التالي  : ^{[ 12 ] : 397}

${\displaystyle {\begin{array}{rcccl}(10):&a\rightarrow b\land ({\textit {true}}\rightarrow d)&\implies &a\rightarrow b\land d&{\mbox{from (1) and (2), with }}p=c\\(11):&a\rightarrow ({\textit {true}}\rightarrow e)&\implies &a\rightarrow e&{\mbox{from (10) and (3), with }}p=(b\land d)\\(12):&\lnot {\textit {true}}&\implies &{\textit {false}}&{\mbox{from (11) and (4), with }}p=(a\rightarrow e)\\\end{array}}}$

من خلال مقارنة كلا الاستنتاجين، يمكن ملاحظة المشكلات التالية:

• قد تُنتج قاعدة تراوغوت مُحلِّلاً أدق: قارن بين (5) و(10)، حيث يُحلِّل كلاهما (1) و(2) على${\displaystyle p=c}$.
• أدخلت قاعدة موراي 3 رموز فصل جديدة: في (5) و(6) و(7)، بينما لم تقدم قاعدة تراوغوت أي رمز جديد؛ وبهذا المعنى، فإن الصيغ الوسيطة لتراوغوت تشبه أسلوب المستخدم بشكل أوثق من موراي.
• بسبب هذه المشكلة الأخيرة، يمكن لقاعدة تراوغوت الاستفادة من الدلالة الواردة في الافتراض (4)، باستخدام كـ${\displaystyle p}$الصيغة غير الذرية${\displaystyle a\rightarrow e}$في الخطوة (12). باستخدام قواعد موراي، الصيغة المكافئة دلاليًا${\displaystyle e\lor \lnot a\lor \lnot a}$تم الحصول عليها كـ (7)، ومع ذلك، لا يمكن استخدامها كـ${\displaystyle p}$بسبب شكلها النحوي.

بالنسبة لمنطق المسند من الدرجة الأولى ، يتم تعميم قاعدة موراي للسماح بصيغ فرعية متميزة، ولكنها قابلة للتوحيد.${\displaystyle p_{1}}$و${\displaystyle p_{2}}$ل${\displaystyle F}$و${\displaystyle G}$، على التوالي. إذا${\displaystyle \phi }$وهو العامل الأكثر عمومية لتوحيد${\displaystyle p_{1}}$و${\displaystyle p_{2}}$إذن، يكون المُحلِّل المُعمَّم هو${\displaystyle F\phi [{\textit {true}}]\lor G\phi [{\textit {false}}]}$بينما تبقى القاعدة سليمة في حالة وجود بديل أكثر خصوصية${\displaystyle \phi }$في حالة استخدام هذه القاعدة، لا حاجة لتطبيقات مثل هذه القاعدة لتحقيق الاكتمال.

تم تعميم قاعدة تراوغوت للسماح بعدة صيغ فرعية متميزة ثنائياً.${\displaystyle p_{1},\ldots ,p_{m}}$ل${\displaystyle F}$و${\displaystyle p_{m+1},\ldots ,p_{n}}$ل${\displaystyle G}$طالما${\displaystyle p_{1},\ldots ,p_{n}}$لنفترض أن يكون هناك عامل موحد عام مشترك.${\displaystyle \phi }$يتم الحصول على المذيب المعمم بعد تطبيق${\displaystyle \phi }$إلى الصيغ الأصلية، مما يجعل النسخة الافتراضية قابلة للتطبيق. يعتمد برهان اكتمال تراوغوت على افتراض استخدام هذه القاعدة العامة تمامًا؛ ^{[ 12 ] : 401،} وليس من الواضح ما إذا كانت قاعدته ستظل كاملة إذا اقتصرت على${\displaystyle p_{1}=\cdots =p_{m}}$و${\displaystyle p_{m+1}=\cdots =p_{n}}$[ ^{16 ]​}