Hennessy–Milner logic
کمپیوٹر سائنس میں، ہینسی ملنر منطق (ایچ ایم ایل) ایک متحرک منطق ہے جو لیبلڈ ٹرانزیشن سسٹم (ایل ٹی ایس) کی خصوصیات کی وضاحت کے لیے استعمال ہوتی ہے، جو ایک آٹومیٹن سے ملتی جلتی ساخت ہے۔ اسے 1980 میں میتھیو ہینسی اور رابن ملنر نے اپنے مقالے "آن آبزرویشن نان ڈیٹرمینزم اینڈ کنکرنسی" (آئی سی اے ایل پی) میں متعارف کرایا تھا۔ ایچ ایم ایل کی ایک اور قسم میں منطق کے اظہار کو بڑھانے کے لیے ریکرشن کا استعمال شامل ہے، اور اسے عام طور پر 'ریکرشن کے ساتھ ہینسی ملنر لاجک' کہا جاتا ہے۔ ریکرشن کو زیادہ سے زیادہ اور کم سے کم فکسڈ پوائنٹس کے استعمال سے فعال کیا جاتا ہے۔ نحو ایک فارمولے کی تعریف مندرجہ ذیل بی این ایف گرائمر سے ایکٹ کے لیے کچھ اعمال کے سیٹ کے ذریعے کی گئی ہے: یعنی، ایک فارمولہ مستقل سچائی ہو سکتا ہے ہمیشہ سچ مستقل غلط ہمیشہ غلط فارمولہ کنجکشن فارمولہ تمام ایکٹ مشتقات کے لیے، φ کو کچھ ایکٹ مشتقات کے لیے فارمولہ رکھنا چاہیے، φ کو رسمی الفاظ رکھنا چاہیے۔ اطمینان بخش تعلق ایل ٹی ایس کی حالتوں کا تعلق اس فارمولے سے کرتا ہے جسے وہ پورا کرتے ہیں، اور اس کی تعریف سب سے چھوٹے تعلق کے طور پر کی جاتی ہے جیسے کہ، تمام حالتوں اور فارمولوں کے لیے، ایسی کوئی حالت نہیں ہے جس کے لیے، اگر ایسی کوئی حالت موجود ہو اور، پھر، اگر ان سب کے لیے جو اسے برقرار رکھتی ہے، تو، اگر، تب، تب، تب، تب، تب، تب۔ موڈل μ-کیلکولس بھی دیکھیں، جو فکسڈ پوائنٹ آپریٹرز ڈائنامک منطق کے ساتھ ایچ ایم ایل کو بڑھاتا ہے، ایک ملٹی موڈل منطق جس میں لامحدود طور پر بہت سے طریقے ہیں۔ 1988۔ "ہینیسی ملنر لاجک ود ریکرشن ایز اے اسپیسیفیکیشن لینگویج، اینڈ اے ریفائنمنٹ کیلکولس بیسڈ آن اٹ"۔ پروسیڈنگز آف دی بی سی ایس-ایف اے سی ایس ورکشاپ آن سپیسیفیکیشن اینڈ ویریفیکیشن آف کنکرنٹ سسٹمز میں، چارلس ریٹری (ایڈ۔)۔ سپرنگر-ورلاگ، لندن، برطانیہ، 294-330۔ ہم آہنگی (کمپیوٹر سائنس) رسمی تفصیلات کمپیوٹر سائنس میں ماڈل منطق منطق