همانطور که فرمودید یکی از روش های اثبات استلزام از طریق برهان خلف است.
یعنی برای اثبات استلزام [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