الگوریتم استنتاج (ایجاب) در منطق گزاره ای
الگوریتم استنتاج (ایجاب) در منطق گزاره ای
اولین الگوریتم مربوط به استنتاج، روش بازرسی مدل است که تعریف ایجاب (نتیجه گیری ) از KB (پایگاه دانش) را بطور مستقیم پیاده سازی میکند: شمارش مدل ها و بررسی این نکته که آیا در هر مدلی که KB درست است، جمله ای مثل a نیز درست هست یا خیر. مدلها، انتساب های true یا false به هر نماد گزاره ای هستند. یک الگوریتم کلی برای تصمیم گیری در مورد "ایجاب" در منطق گزاره ای در ادامه بررسی خواهیم کرد.
همانند الگوریتم BACKTRACKING-SEARCH که با آن آشنایی دارید، TT-ENTIAL? یک شمارش بازگشتی از فضای متناهی "انتساب به نمادها" را اجرا میکند. این الگوریتم، صحیح است، زیرا مستقیما ایجاب را پیاده سازی میکند، و کامل است، زیرا برای هر KB و a کار میکند و همیشه خاتمه می یابد- فقط "تعدادی محدود" از مدلها برای بررسی وجود دارند.
البته تعدادی محدود همیشه به معنای تعداد کم نیست اگر KB و a دارای n نماد باشند، آنگاه 2n مدل وجود دارد. بنابراین پیچیدگی زمانی الگوریتم برابر با O(2n) است. پیچیدگی فضا فقط O(n) است زیرا شمارش بصورت عمقی انجام میشود. متاسفانه ، ایجاب گزاره ای احتمالا آسانتر از NP نیست. بنابراین هر الگوریتم شناخته شده برای منطق گزاره ای یک پیچیدگی زمانی در بدترین حالت دارد که بر حسب اندازه ی ورودی، نمایی است.
الگوریتم کلی برای تصمیم گیری در مورد "ایجاب" در منطق گزاره ای:
function TT-ENTAILS? (KB,a) returns true or false
inputs : KB, the knowledge base, a sentence in propositional logic
a, the query , a sentence in propositional logic
symbols <-- a list of the proposition symbols in KB and a
return TT-CHECK-ALL(KB, a, symbols, {})
function TT-CHECK-ALL(KB, a, symbols, mdel) returns true or false
if EMPTY?( symbols) then
if PL-TRUE? (KB, mdel) then return PL-TRUE?(a, model)
else return true || when KB is false, always return true
else do
p <-- FIRST (symbols)
rest <-- REST(symbols)
return (TT-CHECK-ALL (KB, a, rest, model U { P = true } ) and TT-CHECK-ALL (KB, a, rest, model U { P = false } ))
