مشكلة اتخاذ القرار

الموسوعة الحرة

في الرياضيات وعلوم الحاسوب ، تُعدّ مسألة القرار (Entscheidungsproblem ) ( بالألمانية : Entscheidungsproblem، وتعني " مسألة القرار " ؛ وتُنطق [ ɛntˈʃaɪ̯dʊŋspʁoˌbleːm ] ) تحديًا طرحه ديفيد هيلبرت وويلهلم أكرمان عام 1928. [ 1 ] وتتطلب هذه المسألة خوارزميةً تأخذ في الاعتبار عبارةً مُدخلةً وتُجيب بـ"نعم" أو "لا" بناءً على ما إذا كانت صالحةً عالميًا، أي صالحةً في كل بنية . وقد أثبت ألونسو تشيرش وآلان تورينج استحالة وجود مثل هذه الخوارزمية عام 1936.

نظرية الاكتمال

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

في عام 1936، نشر ألونزو تشيرش وآلان تورينج ورقتين بحثيتين مستقلتين [ 2 ] تُظهران استحالة إيجاد حل عام لمسألة القرار ، بافتراض أن المفهوم البديهي لـ " قابل للحساب فعليًا " يتم تجسيده بواسطة الدوال القابلة للحساب بواسطة آلة تورينج (أو بشكل مكافئ، بواسطة تلك القابلة للتعبير عنها في حساب لامدا ). يُعرف هذا الافتراض الآن باسم أطروحة تشيرش-تورينج .

تاريخ

يعود أصل مسألة القرار إلى غوتفريد لايبنتز ، الذي حلم في القرن السابع عشر، بعد أن بنى آلة حاسبة ميكانيكية ناجحة ، ببناء آلة قادرة على معالجة الرموز لتحديد قيم الصواب للعبارات الرياضية. [ 3 ] أدرك لايبنتز أن الخطوة الأولى تكمن في لغة رسمية واضحة ، ولذا وُجِّه جزء كبير من عمله اللاحق نحو هذا الهدف. في عام 1928، طرح ديفيد هيلبرت وويلهلم أكرمان السؤال بالصيغة الموضحة أعلاه.

استكمالاً لبرنامجه، طرح هيلبرت ثلاثة أسئلة في مؤتمر دولي عام 1928، عُرف السؤال الثالث منها باسم "مسألة هيلبرت في اتخاذ القرار ". [ 4 ] وفي عام 1929، نشر موسى شونفينكل ورقة بحثية حول حالات خاصة من مسألة اتخاذ القرار، أعدها بول بيرنايز . [ 5 ]

حتى عام 1930، كان هيلبرت يعتقد أنه لن يكون هناك شيء اسمه مشكلة لا يمكن حلها. [ 6 ]

إجابة سلبية

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

ثم قدم ألونزو تشيرش إجابة سلبية لمسألة القرار في الفترة 1935-1936 ( نظرية تشيرش )، وبعد ذلك بوقت قصير، قدم آلان تورينج إجابة مستقلة في عام 1936 ( برهان تورينج ). أثبت تشيرش أنه لا توجد دالة قابلة للحساب تُحدد، بالنسبة لتعبيرين معطيين في حساب لامدا، ما إذا كانا متكافئين أم لا. وقد اعتمد بشكل كبير على أعمال سابقة لستيفن كلين . اختزل تورينج مسألة وجود "خوارزمية" أو "طريقة عامة" قادرة على حل مسألة القرار إلى مسألة وجود "طريقة عامة" تُحدد ما إذا كانت أي آلة تورينج معينة ستتوقف أم لا ( مسألة التوقف ). إذا فُهم مصطلح "الخوارزمية" على أنه طريقة يمكن تمثيلها كآلة تورينج، وكانت الإجابة على السؤال الأخير سلبية (بشكل عام)، فإن السؤال حول وجود خوارزمية لمسألة القرار يجب أن تكون سلبية (بشكل عام) أيضًا. في بحثه المنشور عام 1936، يقول تورينج: "بالنسبة لكل آلة حاسوبية 'it'، نبني صيغة 'Un(it)' ونبين أنه إذا كانت هناك طريقة عامة لتحديد ما إذا كانت 'Un(it)' قابلة للإثبات، فستكون هناك طريقة عامة لتحديد ما إذا كانت 'it' تطبع 0 في أي وقت".

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

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

التعميمات

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

شظايا

بشكل افتراضي، تكون المراجع في هذا القسم مأخوذة من برات-هارتمان (2023). [ 7 ]

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

بعض الملاحظات:Sأت(Φ){\displaystyle {\rm {{Sat}(\Phi )}}}يعني ذلك مشكلة تحديد ما إذا كان هناك نموذج لمجموعة من الصيغ المنطقيةΦ{\displaystyle \Phi }.FأنانSأت(Φ){\displaystyle {\rm {{FinSat}(\Phi )}}}هي نفس المشكلة، ولكن بالنسبة للنماذج المحدودة .Sأت{\displaystyle {\rm {Sat}}}تُسمى المسألة المتعلقة بجزء منطقي قابلة للتقرير إذا وُجد برنامج قادر على اتخاذ القرار، لكلΦ{\displaystyle \Phi }مجموعة محدودة من الصيغ المنطقية في الجزء، سواءSأت(Φ){\displaystyle {\rm {{Sat}(\Phi )}}}أو لا.

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

أرسطوية وعلاقاتية

يُصنّف المنطق الأرسطي أربعة أنواع من الجمل: "كل p هي q"، "كل p ليست q"، "بعض p هي q"، "بعض p ليست q". ويمكننا صياغة هذه الأنواع من الجمل كجزء من منطق الرتبة الأولى.∀x،ص(x)→±q(x)،∃x،ص(x)∧±q(x){\displaystyle \forall x,p(x)\to \pm q(x),\quad \exists x,p(x)\wedge \pm q(x)}أينص،q{\displaystyle p,q}هي مسندات ذرية، و+q:=q،-q:=¬q{\displaystyle +q:=q,\;-q:=\neg q}بالنظر إلى مجموعة منتهية من صيغ المنطق الأرسطي، فإن تحديدها يكون مسألة كاملة من حيث NLOGSPACESأت{\displaystyle {\rm {Sat}}}كما أن اتخاذ القرار مكتمل في فضاء NLOGSPACESأت{\displaystyle {\rm {Sat}}}لتوسيع طفيف (النظرية 2.7):∀x،±ص(x)→±q(x)،∃x،±ص(x)∧±q(x){\displaystyle \forall x,\pm p(x)\to \pm q(x),\quad \exists x,\pm p(x)\wedge \pm q(x)}يُوسّع المنطق العلائقي المنطق الأرسطي من خلال السماح باستخدام محمول علائقي. على سبيل المثال، يمكن كتابة عبارة "الجميع يحب شخصًا ما" على النحو التالي:∀x،بoدy(x)،∃y،بoدy(y)∧لovهـ(x،y){\textstyle \forall x,{\rm {{body}(x),\exists y,{\rm {{body}(y)\wedge {\rm {{love}(x,y)}}}}}}}بشكل عام، لدينا 8 أنواع من الجمل:∀x،ص(x)→(∀y،q(x)→±ر(x،y))،∀x،ص(x)→(∃y،q(x)∧±ر(x،y))∃x،ص(x)∧(∀y،q(x)→±ر(x،y))،∃x،ص(x)∧(∃y،q(x)∧±ر(x،y)){\displaystyle {\begin{aligned}\forall x,p(x)\to (\forall y,q(x)\to \pm r(x,y)),&\quad \forall x,p(x)\to (\exists y,q(x)\wedge \pm r(x,y))\\\exists x,p(x)\wedge (\forall y,q(x)\to \pm r(x,y)),&\quad \exists x,p(x)\wedge (\exists y,q(x)\wedge \pm r(x,y))\end{aligned}}}إنها NLOGSPACE - كاملة لتحديدهاSأت{\displaystyle {\rm {Sat}}}(النظرية 2.15). يمكن توسيع المنطق العلائقي ليشمل 32 نوعًا من الجمل عن طريق السماح±ص،±q{\displaystyle \pm p,\pm q}، لكن هذا الامتداد كامل من حيث الوقت (النظرية 2.24).

أريتي

جزء من منطق الرتبة الأولى حيث تكون أسماء المتغيرات الوحيدة هيx،y{\displaystyle x,y}هي مسألة كاملة من نوع NEXPTIME (النظرية 3.18). معx،y،z{\displaystyle x,y,z}، من الضروري تحديد ذلكSأت{\displaystyle {\rm {Sat}}}، وإعادة إكمالها لاتخاذ القرارFأنانSأت{\displaystyle {\rm {FinSat}}}(النظرية 3.15)، وبالتالي غير قابلة للتقرير.

حساب المسند الأحادي هو جزء من الحساب حيث تحتوي كل صيغة على مسندات أحادية فقط ولا تحتوي على رموز دوال. Sأت{\displaystyle {\rm {Sat}}}هي NEXPTIME-كاملة (النظرية 3.22).

بادئة الكمية

لكل صيغة من الدرجة الأولى شكل طبيعي سابق. ولكل بادئة كمية ممكنة للشكل الطبيعي السابق، لدينا جزء من منطق الدرجة الأولى. على سبيل المثال، فئة بيرنايز-شونفينكل ،[∃*∀*]={\displaystyle [\exists ^{*}\forall ^{*}]_{=}}، هي فئة من الصيغ من الدرجة الأولى ذات البادئة الكمية∃⋯∃∀⋯∀{\displaystyle \exists \cdots \exists \forall \cdots \forall }، رموز المساواة والعلاقات، ولا توجد رموز للدوال .

فعلى سبيل المثال، لاحظت ورقة تورينج البحثية لعام 1936 (صفحة  263) أن مشكلة التوقف لكل آلة تورينج تُكافئ صيغة منطقية من الدرجة الأولى على النحو التالي: ∀∃∀∃6{\displaystyle \forall \exists \forall \exists ^{6}}المشكلةSأت(∀∃∀∃6){\displaystyle {\rm {{Sat}(\forall \exists \forall \exists ^{6})}}}غير قابل للحسم.

الحدود الدقيقة معروفة بوضوح:

  • Sأت(∀∃∀){\displaystyle {\rm {{Sat}(\forall \exists \forall )}}}وSأت([∀∃∀]=){\displaystyle {\rm {{Sat}([\forall \exists \forall ]_{=})}}}مكتملة بشكل مشترك، وFأنانSأت{\displaystyle {\rm {FinSat}}}المسائل كاملة RE (النظرية 5.2).
  • وينطبق الأمر نفسه على∀3∃{\displaystyle \forall ^{3}\exists }(النظرية 5.3).
  • ∃*∀2∃*{\displaystyle \exists ^{*}\forall ^{2}\exists ^{*}}قابلة للتقرير، وقد أثبت ذلك بشكل مستقل كل من غودل وشوت وكالمار .
  • [∀2∃]={\displaystyle [\forall ^{2}\exists ]_{=}}غير قابل للحسم.
  • لأين≥0{\displaystyle n\geq 0}، كلاهماSأت(∃ن∀*){\displaystyle {\rm {{Sat}(\exists ^{n}\forall ^{*})}}}وSأت([∃ن∀*]=){\displaystyle {\rm {{Sat}([\exists ^{n}\forall ^{*}]_{=})}}}هي كاملة NEXPTIME (النظرية 5.1).
    • وهذا يعني أنSأت([∃*∀*]=){\displaystyle {\rm {{Sat}([\exists ^{*}\forall ^{*}]_{=})}}}قابلة للتقرير، وهي نتيجة نشرها بيرنايز وشونفينكل لأول مرة. [ 9 ]
  • لأين≥0،م≥2{\displaystyle n\geq 0,m\geq 2}،Sأت(∃ن∀∃م){\displaystyle {\rm {{Sat}(\exists ^{n}\forall \exists ^{m})}}}هو EXPTIME-complete (القسم 5.4.1).
  • لأين≥0{\displaystyle n\geq 0}،Sأت([∃ن∀∃*]=){\displaystyle {\rm {{Sat}([\exists ^{n}\forall \exists ^{*}]_{=})}}}هو NEXPTIME-complete (القسم 5.4.2).
    • وهذا يعني أنSأت(∃*∀*∃*){\displaystyle {\rm {{Sat}(\exists ^{*}\forall ^{*}\exists ^{*})}}}قابلة للتقرير، وهي نتيجة نشرها أكرمان لأول مرة. [ 10 ]
  • لأين≥0{\displaystyle n\geq 0}،Sأت(∃ن∀∃){\displaystyle {\rm {{Sat}(\exists ^{n}\forall \exists )}}}وSأت([∃ن∀∃]=){\displaystyle {\rm {{Sat}([\exists ^{n}\forall \exists ]_{=})}}}هي كاملة وفقًا لمعيار PSPACE (القسم 5.4.3).

يصف بورجر وآخرون (2001) [ 11 ] مستوى التعقيد الحسابي لكل جزء ممكن مع كل تركيبة ممكنة من بادئة الكمية، والعدد الوظيفي، وعدد المسند، والمساواة/عدم المساواة.

إجراءات اتخاذ القرار العملية

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

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

انظر أيضاً

ملحوظات

  1. ^ ديفيد هيلبرت وويلهلم أكرمان. Grundzüge der Theoretischen Logik. سبرينغر، برلين، ألمانيا، 1928. الترجمة الإنجليزية: ديفيد هيلبرت وويلهلم أكرمان. مبادئ المنطق الرياضي. إيه إم إس تشيلسي للنشر، بروفيدنس، رود آيلاند، الولايات المتحدة الأمريكية، 1950
  2. ↑ قُدِّمت ورقة تشرش إلى الجمعية الرياضية الأمريكية في 19 أبريل 1935 ونُشرت في 15 أبريل 1936. شعر تورينج، الذي أحرز تقدمًا كبيرًا في كتابة نتائجه الخاصة، بخيبة أمل عندما علم ببرهان تشرش عند نشره (انظر المراسلات بين ماكس نيومان وتشرش في أوراق ألونسو تشرش ). أكمل تورينج ورقته بسرعة وسارع بنشرها؛ استلمتها وقائع الجمعية الرياضية في لندن في 28 مايو 1936، وقُرئت في 12 نوفمبر 1936، ونُشرت في السلسلة 2، المجلد 42 (1936-1937)؛ ظهرت في قسمين: في الجزء 3 (الصفحات 230-240)، الصادر في 30 نوفمبر 1936 وفي الجزء 4 (الصفحات 241-265)، الصادر في 23 ديسمبر 1936؛ أضاف تورينج تصحيحات في المجلد 43 (1937)، الصفحات 544-546. انظر الحاشية في نهاية كتاب سواري: 1996.
  3. ↑ ديفيس 2001 ، الصفحات 3-20 
  4. ↑ هودجز 1983 ، ص 91 
  5. ↑ كلاين، جي إل؛ أنوفسكا، إس إيه (1951)، "مراجعة لكتاب أسس الرياضيات والمنطق الرياضي لس. أ. يانوفسكايا"، مجلة المنطق الرمزي ، 16 (1): 46-48 ، doi : 10.2307/2268665 ، JSTOR 2268665 ، S2CID 119004002  
  6. ↑ هودجز 1983 ، ص 92 ، نقلاً عن هيلبرت 
  7. 1 2 برات-هارتمان، إيان (30 مارس 2023). شذرات من منطق الرتبة الأولى . مطبعة جامعة أكسفورد. ISBN 978-0-19-196006-2.
  8. ↑ ب. تراختنبروت. استحالة وجود خوارزمية لمسألة القرار للنماذج المحدودة . دوكلادي أكاديميا ناوك، 70: 572-596، 1950. الترجمة الإنجليزية: سلسلة ترجمات الجمعية الرياضية الأمريكية 2، المجلد 33 (1963)، الصفحات 1-6.
  9. ^ بيرنيز ، بول. شونفينكل ، موسى (ديسمبر 1928). "Zum Entscheidungsproblem der mathematischen Logik" . Mathematische Annalen (باللغة الألمانية). 99 (1): 342-372 . دوى : 10.1007 / BF01459101 . ISSN 0025-5831 . S2CID 122312654 .  
  10. ^ أكرمان ، فيلهلم (1 ديسمبر 1928). "Über die Erfüllbarkeit gewisser Zählausdrücke" . Mathematische Annalen (باللغة الألمانية). 100 (1): 638-649 . دوى : 10.1007 / BF01448869 . ردمك 1432-1807 . S2CID 119646624 .  
  11. ^ بورجر، إيغون. جرادل، إريك. جوريفيتش، يوريج. جورفيتش، يوري (2001). مشكلة القرار الكلاسيكية . Universitext (2. طباعة 1. ed.). برلين: سبرينغر. رقم ISBN  978-3-540-42324-9.

مراجع

  • هيلبرت, ديفيد ; أكرمان، فيلهلم (1928). Grundzüge der theoretischen Logik [ مبادئ المنطق الرياضي ] (باللغة الألمانية). سبرينغر-فيرلاغ . رقم ISBN 0821820249.{{cite book}}عدم توافق رقم ISBN / التاريخ ( مساعدة )
  • أكرمان، فيلهلم (1954). الحالات القابلة للحل لمشكلة القرار . أمستردام: نورث هولاند.
  • ألونزو تشيرش ، "مشكلة غير قابلة للحل في نظرية الأعداد الأولية "، المجلة الأمريكية للرياضيات ، 58 (1936)، ص 345-363
  • ألونزو تشيرش ، "ملاحظة حول مشكلة القرار"، مجلة المنطق الرمزي، 1 (1936)، ص 40-41.
  • ديفيس، مارتن (2001). محركات المنطق: علماء الرياضيات وأصل الحاسوب . غلاف ورقي من نورتون (الطبعة الأولى بغلاف ورقي من نورتون  ). نيويورك، نيويورك. لندن: نورتون. ISBN 978-0-393-32229-3.
  • آلان تورينج ، " حول الأعداد القابلة للحساب، مع تطبيق على مسألة القرار "، وقائع الجمعية الرياضية بلندن ، السلسلة 2، 42 (1936-1937)، الصفحات 230-265. النسخ الإلكترونية: من موقع المجلة ، ومن أرشيف تورينج الرقمي ، ومن abelard.org . ظهرت التصويبات في السلسلة 2، 43 (1937)، الصفحات 544-546.
  • ديفيس، مارتن ، "غير القابل للتقرير: أوراق أساسية حول القضايا غير القابلة للتقرير، والمسائل غير القابلة للحل، والدوال القابلة للحساب"، دار رافين للنشر، نيويورك، 1965. ورقة تورينج هي رقم 3 في هذا المجلد. وتشمل الأوراق أوراقًا لغودل، وتشرش، وروسر، وكلين، وبوست.
  • هودجز، أندرو (1983). آلان تورينج: اللغز . نيويورك: سيمون وشوستر. ISBN 978-0-671-49207-6.سيرة آلان م. تورينج. انظر الفصل "روح الحقيقة" للاطلاع على تاريخ أدى إلى برهانه ومناقشته.
  • Soare, Robert I. , "قابلية الحوسبة والتكرار"، نشرة المنطق الرمزي 2 (1996)، العدد 3، 284-321.
  • تولمين، ستيفن ، "سقوط عبقري"، مراجعة كتاب " آلان تورينج: اللغز " لأندرو هودجز، في مراجعة نيويورك للكتب، 19 يناير 1984، ص  3 وما بعدها.
  • وايت هيد، ألفريد نورث ؛ راسل، برتراند ، كتاب "برينسيبيا ماثيماتيكا" إلى الصفحة 56، كامبريدج، مطبعة الجامعة، 1962. فيما يتعلق بمشكلة المفارقات، يناقش المؤلفان مشكلة عدم كون المجموعة كائنًا في أي من "وظائفها المحددة"، وتحديدًا "المقدمة، الفصل 1، صفحة 24 "...الصعوبات التي تنشأ في المنطق الصوري"، والفصل 2.1 "مبدأ الحلقة المفرغة"، صفحة  37 وما بعدها، والفصل 2.8 "التناقضات"، صفحة  60 وما بعدها.
  • شعار ويكشنريتعريف كلمة entscheidungsproblem في قاموس ويكشنري