اصول سیستم های خبره – فصل ۲: گزرد و منطق

اصول سیستم های خبره – فصل ۲: گزرد و منطق – ایران ترجمه – Irantarjomeh

مقالات ترجمه شده آماده گروه کامپیوتر

مقالات ترجمه شده آماده کل گروه های دانشگاهی

مقالات

چگونگی سفارش مقاله

الف – پرداخت وجه بحساب وب سایت ایران ترجمه(شماره حساب)ب- اطلاع جزئیات به ایمیل irantarjomeh@gmail.comشامل: مبلغ پرداختی – شماره فیش / ارجاع و تاریخ پرداخت – مقاله مورد نظر --مقالات آماده سفارش داده شده پس از تایید به ایمیل شما ارسال خواهند شد.

www.irantarjomeh.com

اصول سیستم های خبره

فصل ۲٫ گزرد و منطق

یکی از اولین فرمول بندی ها برای نمایش دانش منطق است. فرمول بندی با استفاده از یک ترکیب و معناشناسی معین مشخص شده است و برخی از قواعد استنتاجی را برای تغییر فرمول های منطقی بر مبنای فرم آنها مشخص می کند تا شناخت جدیدی حاصل شود. منطق یک سنت غنی و طولانی دارد که به یونان قدیم برمی گردد : ریشه آن را می توان به ارسطو نسبت داد. با این حال تداوم این مورد را می توان تا قرن حاضر در نظر گرفت یعنی زمانی که اصول ریاضی منطق مدرن بوسیله ریاضیدانانی نظیرT. Skolem ، J.
Herbrand ، K. G¨odel  و G. Gentzen  بنیان گذاشته شد. کار این ریاضیدانان بزرگ عرضه کامل منطق قبل از پدیدار شدن علوم کامپیوتری بود.

از اوایل دهه پنجاه، به مجرد ارائه کامپیوترهای دیجیتال نسل اول تحقیق در مورد استفاده از منطق برای حل مسئله با ابزارهای کامپیوتری آغاز شد. این تحقیق با توجه به دیدگاه های مختلف در نظر گرفته شد. چندین محقق عمدتا به مکانیزاسیون اثبات های ریاضی علاقه مند بودند و تولید خودکار کارآمد چنین اثبات هایی هدف اصلی آنها تلقی شد. یکی از این متخصصین دکتر ام. دیویس می باشد که در سال ۱۹۵۴ یک برنامه کامپیوتری را ابداع کرد که قادر به اثبات چندین قضیه از برخی نظریات بود. بزرگترین پیروزی از برنامه اثبات آن بود که حاصل جمع دو عدد زوج نهایتا زوج می باشد. محققان دیگر، با این حال،  بیشتر به مطالعه و حل مشکلات بشری و اکتشاف موارد علاقه نشان می دادند. برای این محققان، استدلال ریاضی به عنوان یک نقطه عزیمت در خصوص مطالعه اکتشافی بشمار آمده و منطق نیز بعنوان جوهره ریاضیات مشخص شد که صرفا به عنوان یک زبان مناسب برای نمایش رسمی استدلال انسانی بکار می رود. مثال کلاسیک این رویکرد در این زمینه اثبات قضیه یک برنامه تهیه شده در سال ۱۹۵۵ بوسیله A. Newell ، J.C. Shaw  و H.A. Simon  با نام ماشین تئوری منطق بود. این برنامه قادر به اثبات چندین قضیه مرتبط با اصول ریاضیات A.N. Whitehead و B. Russell بود. در ابتدای سال ۱۹۶۱، مک کارتی (J. McCarthy )  و همراه با افراد دیگری اظهار می کنند که این اثبات قضیه را می توان برای حل مسائل غیر ریاضی نیز بکار برد. این ایده توسط محققان متعدد بکار رفت.

پس از برخی موفقیت های اولیه، مشخص شد که قواعد استنتاج مشخص شده در این زمان برای کاربرد در کامپیوترهای دیجیتال مناسب نیست. بسیاری از محققان هوش مصنوعی علاقه خود در بکارگیری منطق را از دست دادند و توجه خود را به سمت رشد فرمول های دیگر برای یک نمایش کارآمد و دستکاری اطلاعات معطوف کردند. دستیابی به موفقیت به لطف توسعه یک قاعده استنتاج انعطاف پذیر و کارآمد در سال ۱۹۶۵ با نام گزرد بود که اجرای منطق برای حل مسئله خودکار با کامپیوتر و اثبات قضیه را میسر می کرد که موقعیت مناسبی را در هوش مصنوعی بدست آورد و اخیرا در زمینه علوم کامپیوتر به عنوان یک کل بکار گرفته شد.

منطق به طور مستقیم می تواند به عنوان یک فرمول بندی مشخص برای ساخت سیستم های خبره بکار می رود ؛ با این حال در حال حاضر تنها در یک مقیاس کوچک اجرا شده است. اما بعدها معنایی مشخص منطق فرمول بندی را به عنوان یک نقطه عزیمت برای شناخت آنچه فرمول بندی شاخص دانش ذکر می شود در نظر گرفت. در این فصل، ما ابتدا به موضوع نحوه نمایش دانش در منطق و حرکت از منطق گزاره ای می پردازیم که اگرچه دارای یک بیان محدوداست، برای معرفی مفاهیم خیلی مفید دیگر خیلی مفید است. منطق پیش بینی مرتبه اول، که یک زبان غنی تر را برای نمایش دانش ارائه می کند، در بخش ۲٫۲ ذکر شده است. بخش اصلی این مقاله به جنبه های الگوریتمی اجرای منطق در یک سیستم استدلال خودکار و گزرد مربوط می شود که موضوع این تحقیق است.

اصول سیستم های خبره – فصل ۲: گزرد و منطق

۲٫۱ منطق گزاره ای

منطق گزاره ای ممکن است به عنوان یک زبان نمادین در نظر گرفته شود که به ما اجازه می دهد تا با گزینه هایی استدلال کنیم که درست یا نادرست هستند. مثال هایی از چنین گزینه هایی شامل :

آئوریت یک رگ بزرگ است.

گزینه هایی نظیر موارد فوق گزاره هایی نامیده می شوند که معمولا در منطق گزاره ای با حروف بزرگ نشان داده می شوند. گزاره های ساده نظیر P و Q گزاره های اتمی یا بطور اختصار اتم ها نامیده می شوند. اتم ها می توانند با اتصالات منطقی ترکیب شوند تا نسبت های ترکیبی حاصل شود. در زبان منطق گزاره ای، ۵ ارتباط زیر را در اختیار داریم :

منفی ¬

متصل ∧

منفصل ∨

مفهوم →

دو مفهومی ↔

برای مثال، زمانی که فرض می کنیم گزاره های G  و  D معنای زیر را دارند

G = آئورت یک رگ بزرگ است.

D= آئوریتن یک قطر برابر با ۲٫۵ سانتی متر دارد.

پس، نسبت ترکیبی

G ∧ D

معنای زیر را دارد :

آئوریت یک رگ بزرگ است و قطر ۲٫۵ سانتی متر دارد.

با این حال تمامی فرمول ها حاوی اتم ها نیستند و اصلاحات گزاره ها هستند. برای تشخیص درست فرمول هایی که گزاره ها را از این موارد نشان می دهند، مفهوم یک فرمول مشخص در تعریف زیر ذکر شده است.

اصول سیستم های خبره – فصل ۲: گزرد و منطق

۲٫۲٫ منطق گزاره ای مرتبه اول

در منطق گزاره ای، اتم ها تشکل های بنیادی فرمول ها هستند که درست یا نادرست هستند. یک محدودیت منطق گزاره ای عدم امکان پذیر بودن بیان گزینه های کلی مربوط به موارد مشابه است. منطق گزاره ای مرتبه اول توصیفی تر از منطق گزاره ای است و این گزینه های کلی می توانند در زبان خود مشخص شوند. ابتدا اجازه دهید زبان منطق گزاره ای مرتبه اول را معرفی کنیم. نمادهای زیر بکار رفته اند :

* نمادهای گزاره ای  ،معمولا با  حروف بزرگ نشان داده می شود. هر نماد گزاره ای یک ارتباط با عدد طبیعی n, n ≥ ۰, را دارد که تعداد آرگومان های نماد گزاره ای را نشان می دهد ؛ نماد گزاره ای یک نماد گزاره ای مکان n، مکان ۰ یا معمولا نمادهای گزاره ای نامیده می شوند. نمادهای گزاره ای یک مکان، دو مکان، سه مکان می بانشد که نمادهای گزاره ای یک تایی، دوتایی و سه تایی نامیده می شوند.

* متغیرها، معمولا با حروف بزرگ از انتهای الفبا نشان داده می شوند مثل x,y,z که احتمالا با یک عدد طبیعی شاخص گذاری شده اند

* نمادهای تابع، معمولا با حروف کوچک الفبا نشان داده می شوند. هر نماد تابع با یک عدد طبیعی n, n ≥ ۰, مرتبط است که عدد و آرگومان را نشان می دهد ؛ نماد تابع مکان n نامیده می شود. نمادهای تابع Nullary معمولا ضرایب ثابت نامیده شده اند.

* اتصال منطقی که در بخش قبلی بحث شده اند.

* دو محاسبه کننده : محاسبه کننده کلی ∀ و محاسبه گر موجود ∃ . محاسبه گر باید به صورت زیر خوانده شود : اگر x یک متغیر است، پس ∀x برای هر x’ یا برای تمامی x و ∃x به معنای وجود یک x می باشد.

* برخی از نمادهای کمکی نظیر پرانتزها و ویرگول ها.

متغیرها و توابع در منطق کم و بیش مشابه با متغیرها و توابع در محاسبه و جبر می باشند.

قبل از این که مفهوم یک فرمول اتمی را در منطق گزاره ای مشخص کنیم، اول مفهوم یک عبارت را معرفی می کنیم.

تعریف ۲٫۶٫ یک عبارت به صورت زیر تعریف شده است :

۱) یک ضریب ثابت یک عبارت است.

۲) یک متغیر یک عبارت است.

۳) اگر یک نماد تابع جایگذاری n باشد، n ≥ ۱ و ۱, . . . , tn عبارت ها هستند، پس f(t1, . . . , tn) یک عبارت است.

۴) هیچ چیز دیگری یک عبارت نیست.

بنابراین یک عبارت ضریب ثابت یا متغیر یا تابعی از موارد است. به یاد بیاوردید که یک ضریب ثابت ممکن است به عنوان یک نماد تابع نولاری در نظر گرفته شود. یک فرمول اتمی اکنون شامل یک نماد گزاره ای و برخی از عبارات در نظر گرفته شده به عنوان آرگومان های نماد گزاره است.

اصول سیستم های خبره – فصل ۲: گزرد و منطق

۲٫۳٫ فرم گزاره ای منطق

قبل از این که به استدلال در منطق بپردازیم، در این بخش یک فرم محدود نحوی از منطق مسندی با نام فرم گزاره ای منطق را نشان می دهیم که نقش مهمی را در ادامه این فصل دارد. این فرم محدود می تواند به عنوان منطق مسندی مرتبه اول در نظر گرفته شود. فرم گزاره منطق غالبا بطور خاص در زمینه ای قضیه ارائه کننده برنامه نویسی منطقی بکار رفته است.

ما کار را با تعریف برخی مفاهیم جدید شروع می کنیم.

تعریف ۲٫۱۳٫ یک لفظ یک اتم به نام یک لفظ مثبت یا نفی یک اتم است، یا یک لفظ از یک اتم با نام لفظ منفی است.

تعریف ۲٫۱۴٫ یک گزاره یک فرمول بسته از فرم زیر است

که در آن هر  یک لفظ با  برای هر  است و ،  متغیرهای رویداد در  هستند. اگر  باشد، عبارت تهی  است.

عبارت تهی  به صورت یک فرمول تفسیر شده است که همواره نادرست است، یعنی  یک فرمول نامطلوب است.

۲٫۴٫ استدلال در منطق : قواعد استنتاج

در بخش های ۲٫۱ و ۲٫۲ نشان دادیم چگونه یک معنا می تواند با یک مجموعه معنایی از فرمول های منطقی ارتباط داشته باشد. این کار گاهی اوقات معنای اظهاری منطق نامیده می شود. معناشناسی اعلانی ابزاری برای بررسی مثالی است که آیا یک فرمول مشخص یک نتیجه منطقی از مجموعه ای از فرمول ها است یا خیر . با این حال، امکان جواب دادن به این سوال بدون بررسی محتویات معنایی فرمول های مورد نظر وجود دارد که با اجرای قواعد استنتاج انجام می شود. در مقابل با جداول حقیقی، قواعد استنتاج عملگرهای صرفا معنایی هستند که تنها قادر به اصلاح فرم عناصر یک مجموعه معین از فرمول ها می باشند. قواعد استنتاج شامل اضافه، جایگزین کردن یا حذف فرمول ها است. بیشتر قواعد استنتاج بحث شده در این کتاب فرمول های جدیدی را به یک مجموعه معین از فرمول ها اضافه می کند. بطور کلی ،یک قاعده استنتاج به عنوان یک الگوی مشخص شده که در ان نوعی فرامتغیر حاصل می شود که ممکن است با فرمول های تصادفی جایگزین شود. یک مثال از چنین الگویی در زیر نشان داده شده است.

۲٫۵٫ گزرد و منطق گزاره ای

ما این بخش را با طرح کلی اصول گزرد شروع می کنیم. به یک مجموعه از فرمول های S در فرم اخباری توجه کنید. فرض کنا یک فرمول معین G را در فرم کلاسیکی داریم که در ان باید ثابت کنیم می توانیم از S با اجرای گزرد مقدار را بدست اوریم. اثبات S ⊢ G برابر با اثبات این مورد است که مجموعه ای از کلاس های w، حاوی گزاره هایی در S کامل شده با لفظ فرمول های G می باشند یعنی W = S ∪{¬G} نامطلوب است. گزرد W اکنون به صورت زیر می آید : اول، کنترل می شود آیا W حاوی گزاره خالی  است یا خیر .اگر این طور باشد، پس W قاعده گزرد اجرا شده در یک زوج مناسب برای گزاره ها از W است، که یک گزاره جدید را به بار می آورد. هر گزاره بدست آمده به این صورت به W اضافه می شود که به مجموعه جدیدی از گزاره ها منجر می شود و در آن روش گزرد مشابه اعمال شده است. روش کامل تا زمانی تکرار می شود که برخی مجموعه های ایجاد شده از گزاره ها حاوی گزاره خاص باشند و نامطلوب بودن W را نشان دهد، یا تا زمانی که تمامی گزاره های جدید مشتق گیری شده باشند. اصول بنیادی گزرد به بهترین شکل با ابزارهای مثال منطق گزاره ای نشان داده شده است. در بخش ۲٫۶ به منطق مسندی بیشتر می پردازیم.

مثال ۲٫۲۰

به مجموعه مسندهای زیر توجه کنید

{C1 = P ∨ R,C2 = ¬P ∨ Q}

این عبارت ها حاوی لفظ های مکمل هستد، یعنی لفظ های دارای مقادیر حقیقی متضاد با نام های P  و  ¬P. با اجرای گزرد، یک گزاره جدید C3 با انفصال گزاره های اصلی C1  و  C2بدست آمده است که در آن عبارت های مکمل حذف شده اند. بنابراین بکارگیری روزلوشن عبارت زیر را در پی دارد

اصل گزرد بطور دقیق تر در تعریف زیر شرح داده شده است.

تعریف ۲٫۱۸ . به دو عبارت C1  و  C2 حاوی کلمات L1  و  L2 توجه کنید که در آن L1  و L2 مکمل هم هستند. روش گزرد به صورت زیر ذکر می شود :

۲٫۶٫ گزرد و منطق مسند مرتبه اول

یک ویژگی مهم از گزرد در منطق سند رده اول، در روش گزرد پایه، دستکاری عبارات است. این مورد با بخش قبلی بکار رفته است، که در آن تنها گزاره های جزیی، اتصالات و نمادهای کمکی را به عنوان بلوک های ساختاری برای فرمول های گزاره ای دارند. در این بخش، اول دستکاری عبارت ها را بحث می کنیم، قبل از این که یک شرح مفصل از گزرد را در منطق مسندی مرتبه اول ذکر کنیم.

۲٫۶٫۱٫ جایگزینی و یکپارچه سازی

جایگزینی عبارت های برای متغیرها در فرمول ها برای ایجاد ترکیب های فرمول های برابر، نقش مهمی در روش موسوم به یکپارچه سازی دارد. اول مفهوم جایگزینی را بطور رسمی معرفی کرده و نقش آن را در واحد سازی بحث می کنیم.

تعریف ۲٫۲۰ . یک جایگزینی a یک مجموعه معین فرم

{t1/x1, . . . , tn/xn}

که در آن هر xi یک متغیر است و این که هر ti یک عبارت غیربرابر با xi, i = 1, . . . , n, n ≥ ۰ است، و متغیرهای x1, . . . , xn از همدیگر متفاوت است. یک عنصر ti/xi یک جایگزین  یک ترکیب برای متغیر xi نام دارد. اگر عبارت های ti در یک جایگزینی حاوی یک متغیر باشد، داریم یک جایگزینی زمینه ای . جایگزینی تعریف شده توسط مجموعه تهی جایگزینی تهی نام دارد و با  نام دارد.

۲٫۶٫۲٫ جایگزینی و یکی سازی در LISP

فرایند جایگزین که در بخش قبلی معرفی شد را می توان به شیوه طبیعی با ابزارهای یک الگویتم اکتشافی شرح داد : الگوریتم جایگزین در یک عبارت عمل می کند که بخودی خود از عبارت های فرعی تشکیل شده است. این ایده مبنای یک برنامه LISP است که در زیر بحث خواهد شد. برنامه عبارت ها را در فرم پیشوند نظیر (P (f x (ga)) y) می پذیرد که برای اتم P(f(x, g(a)), y). بکار می رود. اتم های LISP برای نمایش نمادهای مستندی، نمادهای تابع، ضرایب ثابت و متغیرها بکار می رود.

اصول سیستم های خبره – فصل ۲: گزرد و منطق

۲٫۷٫ راهکارهای گزرد

بیشتر اصول بنیادی گزرد در بخش قبلی بحث شده اند. با این حال یک موضوع خاص با نام کارایی الگوریتم گزرد، بطور صریح مورد توجه قرار نگرفت. لازم نیست بگوییم که موضوع کارایی یک موضوع مهم برای استدلال خودکار است.

متاسفانه، روش نفی کلی معرفی شده در بخش ۲٫۶٫۳کاملا ناکارآمد است، چون در بسیاری از موارد تعداد زیادی از گزاره های اضافی را ایجاد می کند، یعنی گزاره هایی که در مشتق گیری گزاره خالی نقش ندارند.

مثال ۲٫۳۶

به مجموعه گزاره های زیر توجه کنید :

S = {P,¬P ∨ Q,¬P ∨ ¬Q ∨ R,¬R}

برای ساده سازی مربوط به آنها، گزاره ها به صورت زیر شماره گذاری شده اند :

۲٫۷٫۱٫ گزرد معنایی

گزرد معنایی نام یک طبقه از راهکارهای گزرد است که همگی بطور مشترک نشان می دهند که فرایند گزرد توسط معناشناس اعلانی گزاره های پردازش شده کنترل شده است. ما بطور مختصر ایده کلی را شرح داده و برخی فرم های خاص گزرد معنایی را بطور غیررسمی نشان می دهیم .

به یک مجموعه نامطلوب از گزاره های S توجه کنید. امکان تقسیم مجموعه ای از گزاره های S به دو زیرمجموعه مجزا برمبنای یک تفسیر خاصI وجود دارد : زیرمجموعه S1 حاوی گزاره هایی از S است که در I نادرست هستند و زیرمجموعه S2 حاوی گزاره هایی است که در I واقعی هستند. چون S نامطلوب است، هیچ تفسیری تابحال نمی تواند تمامی گزاره های درست یا نادرست را در برگیرد. بنابراین، مجموعه گزاره Sبه  دو زیرمجموعه غیرتهی تقسیم شده است. این تفکیک معنایی می تواند به عنوان مبنای راهکار کنترل بکار رود که در ان یکی از گزاره های خانواده از S1 انتخاب شده و دیگری از S2 . حل کننده ایجاد شده به S1 یا S2 بسته به تفسیر I.افزوده شده است. مثال بعد، بطور خاص در این فرم از روزلوشن نشان داده شده اند.

۲٫۷٫۲٫ گزرد SLD : یک فرم خاص گزرد خطی

گزرد خطی پس از ایجاد ساختار نمودار مشتق توسط این طبقه از راهکارها نام گذاری شده است : در هر مرحله گزرد حل آخر به عنوان یک گزاره خانواده در نظر گرفته شده است. گزاره خانواده دیگر یک گزاره از مجموعه اصلی از گزاره ها یا یک حل کننده است که از قبل ایجاد شده است. یک فرم خاص از گزرد خطی گزرد ورودی است. در این راهکار، هر مرحله گزرد، به استثنای مرحله اول، در حل کننده آخر و یک گزاره از مجموعه اصلی از گزاره ها اجرا شد. گزاره های قبلی گزاره های هدف نامیده می شوند و گزاره های دوم گزاره های ورودی می باشند، بنابراین نام راهکار را شرح می دهند. گزرد ورودی یک راهکار کامل برای گزاره های هورن است ؛ برای فرم گزاره ای منطق، حل ورودی کامل نیست.

اصول سیستم های خبره – فصل ۲: گزرد و منطق

۲٫۱۰ . منطق به عنوان یک فرمول بندی شاخص

در مقایسه با فرمول بندی های شاخص دانش در هوش مصنوعی، منطق مزیت بزرگ دارا بودن نحو و معنای مشخص را دارد. یک سیستم قیاسی منطقی در اصل مجموعه ای ا زقواعد استنتاج را ارائه می کند که کامل و سالم به نظر می رسد. هر فرمول بدست آمده با استفاده از مجموعه ای از قواعد استنتاج معنایی دارد که از لحاظ معنای فرمول ها منحصر به فرد است. بنابراین منطق یک نقطه آغازین را برای بررسی پایه های نمایش دانش و دستکاری ان ارائه می کند.

منطق مرتبه اول در فرم صرف آن بسختی به عنوان یک فرمول بندی شاخص دانش در سیستم های خبره بکار می رود. این مورد بطور نسبی بخاطر مشکل بودن بیان دانش حوزه در فرمول های منطقی است. زمانی که در حوزه مسئله خاص دانش در یک فرم نزدیک به منطقی موجود نیست، انرژی زیادی باید برای تبدیل دانش کارشناسی به فرمول های منطقی تبدیل شود و در این فرایند غالبا اطلاعات ارزشمندی از دست رفته است. علاوه بر این، نوع منطقی که در این فصل مورد توجه قرار گرفت ،که گاهی اوقات منطق استاندارد نامیده می شود استدلال در مورد کدگذاری تمامی انواع دانش است. برای مثال، استدلال در مورد زمان و استدلال در مورد راهکارهای استدلال رعایت شده است که غالبا فرااستنتاج نامیده می شود و نمی تواند بطور مستقیم در منطق مستندی مرتبه اول نشان داده شود . علاوه بر این، در منطق استاندارد امکان مدیریت اطلاعات نامشخص و ناقص یا پرداختن کافی به موارد استثنایی برای قواعد کلی وجود ندارد. با این حال تحقیق زیادی قصد دارد به منطق های غیراستاندارد برای بیان چنین مفاهیمی به شیوه رسمی توجه کند. احتمالا به نظر می رسد که منطق یک جایگاه برجسته تر را در سیستم های خبره نسل آینده ایفا کند.

اصول سیستم های خبره – فصل ۲: گزرد و منطق

مقالات پیشنهادی برای مطالعه

برای معرفی محاسباتی برای منطق و  استنتاج منطقی به خواننده به مراجع  [En–derton72]  و [Dalen83] مراجعه کنید.

برنامه کامپیوتری برای اثبات قضیه توسط دکتر دیویس طراحی شده که ماشین تئوری منطقی را ارائه می کند. این مقالات بازچاپ شده و دو کتاب جالب حاوی مقالات کلاسیک در مورد اثبات قضیه نگاشته شده است. مقالات اولیه در مورد کاربرد تکنیک های اثبات قضیه در سیستم های پاسخ دهی به سوال [Slagle65]  و  [Green68] هستند.