بخشی از متن:
قوانين استنتاج در منطق گزاره اي
قوانين استنتاج: الگوهايي استاندارد که زنجيره اي از نتايج را براي رسيدن به هدف ايجاد ميکند
قانون حذف استلزام يا modus ponens
قانون حذف عطف
قانون معرفي عطف
قانون معرفي فصل
قانون حذف دو منفي
قانون اثبات واحد يا resolution واحد
قانون اثبات يا resolution
1- قانون حذف استلزام يا Modus Ponens
عبارت زير يعني از α=>β و α مي‌توان β را استنتاج کرد.
مثلاً ميتوان از
(WumpusAhead ^ WumpusAlive)
و
(WumpusAhead ^ WumpusAlive) => Shoot
Shoot را استنتاج کرد

الگوريتم resolution
براي اينکه نشان دهيمKB|=a , مشخص ميکنيم (KB ^ ¬a) ارضا کننده نيست
ابتدا (KB ^ ¬ a) را به CNF تبديل ميکنيم
سپس قانون resolution به عبارات کوچک حاصل اعمال ميشود
هر جفتي که شامل ليترالهاي مکمل باشد، resolution ميشود تا عبارت جديدي ايجاد گردد
اگر اين عبارت قبلا در مجموعه نباشد، به آن اضافه ميشود
فرايند تا محقق شدن يکي از شروط زير ادامه مي يابد:
هيچ عبارت ديگري وجود نداشته باشد که بتواند اضافه شود. در اين مورد، b استلزام a نيست
کاربرد قانون resolution، عبارت تهي را بدست ميدهد که در اين مورد، b استلزام a است

فهرست مطالب:
عاملهاي مبتني بر دانش
منطق
منطق گزاره اي
الگوهاي استدلال در منطق گزاره اي
الگوريتم resolution
زنجير پيشرو و عقبگرد