[attachment=21484]
سلام دوستان خسته نباشید. جواب این سوال در کلید سنجش گزینه دوم هست. و در پاسخ نامه ای که دوستان لطف کردند و در مانشت گذاشتند نوشته شده که
در روش DPLL برای اثبات اینکه KB مستلزم Q است از روش برهان خلف استفاده میشود و نشان داده میشود که KB و گزاره Q نمیتوانند باهم همزمان درست باشند. و گزینه دو جواب است
آخه اینا که تعریف الگوریتم resolution هست نه DPLL?
همانطور که فرمودید یکی از روش های اثبات استلزام از طریق برهان خلف است.
یعنی برای اثبات استلزام [tex]KB\: \models\: Q[/tex] آنرا بصورت فرم CNF در میآوریم
یعنی [tex]KB\: \wedge\sim\: Q[/tex]
اگر نتوانیم عبارت فوق را اثبات کنیم نتیجه میگیریم استلزام [tex]KB\: \models\: Q[/tex] برقرار است
خیلی ممنونم ازتون.
در مورد الگوریتم DPLL اول اینکه جمله ی ورودی باید به فرم CNF باشه .دوم اینکه شبیه الگوریتم جستجوی عقبگرد مسائل ارضای محدودیته . سوم اینکه از روش شمارش مدلها برای استنتاج گزاره ای استفاده میکنه و درخت جستجو را به صورت عمقی پیاده سازی میکنه و در هر سطح یکی از سمبلهای گزاره ای رو مقداردهی میکنه. و برای اینکه غیرامیدبخش بودن گره رو زود تشخیص بده از سه هیوریستیک "خاتمه زودهنگام" "سمبل محض" و "عبارت واحد" استفاده میکنه.
آیا نکته ی دیگه ای هم هست ؟ کتاب من همیناس.
۹۴ و ۹۵ در رابطه با dpll سوال اومده
جالبه
Sent from my SM-J710F using Tapatalk