الگوریتم زنجیره پیشرو forward chaining برای منطق گزاره ای

الگوریتم زنجیره پیشرو برای منطق گزاره ای
کامل بودن تحلیل در منطق گزاره ای آن را به یک روش استنتاج مهمی تبدیل کرده است. اما در بسیاری از وضعیتهای عملی به کل قدرت تحلیلی نیاز نداریم. بعضی از پایگاه های دانش در دنیای واقعی، بعضی از محدودیت هایی را که به شکل جملات هستند، ارضا میکنند و در نتیجه آنها را قادر میسازد از الگوریتم های استنتاج محدودتر و کارآمدتری استفاده کنند.
یکی از این شکلهای محدود کلاز معین است که ترکیب فصلی لیترال هایی است که دقیقا یکی از آنها مثبت است.
یک کلاز کلی تر به نام کلاز هورن است، ترکیب فصلی لیترال هایی است که از بین آنها حداکثر یک لیترال مثبت است. بنابراین، تمام کلازهای معین، کلاز هورن هستند، زیرا کلازها فاقد لیترال های مثبت هستند، اینها را کلاز های هدف مینامند. کلازهای هورن تحت تحلیل بسته اند: اگر دو کلاز هورن را حل کنید به یک کلاز هورن میرسید.
استنتاج با کلازهای هورن میتواند از طریق الگوریتمهای زنجیره پیشرو و زنجیره عقبگرد انجام شود. هر یک از این دو الگوریتم طبیعی هستند، زیرا مراحل استنتاج ساده است و انسان میتواند به راحتی آن را دنبال کند. این نوع استنتاج مبنایی برای برنامه نویسی منطقی است.
زنجیره پیشرو
الگوریتم زنجیره پیشرو یعنی PL-FC-ENTAILS?(KB,q) تعیین میکند آیا نماد گزاره ای q (پرس و جو) توسط پایگاه دانشی از کلازهای معین، ایجاب میشود(به دست می آید) یا خیر. این الگوریتم با حقایق معلومی (لیترال های مثبت) در پایگاه دانش شروع می کند. اگر تمام مقدم های ایجاب معلوم باشند (شناخته شده باشند) ، آنگاه تالی (نتیجه ی) آن به مجموعه ای از حقایق معلوم اضافه میشود. این فرآیند آنقدر ادامه می یابد تا پرس و جوی q اضافه شود یا دیگر نتوان حقیقت دیگری را اضافه کرد. الگوریتم مشروح را در ادامه خواهید دید. نکته اصلی که باید به آن توجه کرد این است که این الگوریتم در زمان خطی اجرا میشود.
زنجیره پیشرو صحیح است، یعنی هر استنتاج، اساسا کاربردی از استنتاج قیاسی است. زنجیره پیشرو کامل نیز هست، یعنی هر جمله اتمیک ایجاب شدنی، میتواند به دست آید.
این الگوریتم مثالی از یک مفهوم کلی به نام استدلال مبتنی بر داده ها است، یعنی استدلالی که در آن کار با داده های معلوم آغاز میشود. میتوان از آن مفهوم در داخل عامل برای کسب نتایجی از ادراکات ورودی استفاده کرد.
الگوریتم زنجیره پیشرو برای منطق گزاره ای:
function PL-SC-ENTAILS?(KB,q) returns true or false
inputs : KB, the knowledge base, a set of propositional definite clauses
q, the query, a proposition symbol
count <-- a table, where count [c] is ehe number of symbols in cs premise
inferred <-- a table, where inferred[s] is initially false for all symbols
agenda <-- a queue of symbols, initially symbols jnown to be true in KB
while agenda is not empty do
p <-- POP(agenda)
if p = q then return true
if inferred[p] = false then
inferred[p] <-- true
for each clause c in KB where p is in c.PREMISE do
decrement count[c]
if count[c] = 0 then add c.CONCLUSION to agenda
return false
در این الگوریتم agenda نمادهایی را نگه میدارد که درست هستند ولی هنوز پردازش نشده اند. جدول count مشخص میکند چند مقدم هر ایجاب منطقی هنوز ناشناخته اند. هر وقت نماد جدید p از agenda پردازش میشود count برای هر ایجابی که p در مقدم ان ظاهر میشود، یک واحد کاهش می یابد. اگر count صفر شد تمام مقدمات ایجاب شناخته شده اند و نتیجه اش میتواند به agenda اضافه شود. لازم است بدانیم چه نمادهایی پردازش شدند. اگر نماد استنتاج شده ای پردازش شد، نباید به agenda اضافه شود. به این ترتیب از کار اضافی جلوگیری میکند.