فهرست مطالب :

مقدمه

پایه‌ی منطق محاسباتی

Resolution Propositional

پایه‌ی ریاضی

کاربردهای منطق محاسباتی

• Database Systems

• Software Analysis

• Hardware Engineering

• Automated Theorem Proving

STRIPS

آینده منطق محاسباتی

نتیجه‌گیری

منابع

مقدمه :

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

– پایه‌ی منطق محاسباتی

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

چرچ در ۱۹۳۶ ثابت کرد که منطق مرتبه اول برای زبانی که فقط یک نماد رابطه‌ای دو موضعی داشته باشد تصمیم ناپذیر است. بنا بر قضیه چرچ روشی متناهی برای پاسخ به این سوال که آیا جمله A در منطق مرتبه اول معتبر است، به صورت “آری” یا “نه” نداریم، اما نیمه ای از پاسخ را میتوان مهیا کرد. به عبارت بهتر روشی متناهی وجود دارد که اگر A معتبر باشد، پاسخ روش “آری” است. به عبارت دیگر مجموعه جملات معتبر در منطق مرتبه اول لیست پذیر هستند. از طرف دیگر با توجه به قضیه تمامیت (در صورتی که در مورد دستگاه استنتاجی ما درست باشد) با استفاده از فرضها و اصول استنتاج میتوان جملات درست را لیست کرد. این قسمت در حقیقت قلب تپنده‌ی منطق محاسباتی است. در صورت پیدا شدن روشهای جدید و سریعتر برای چک کردن درستی یک جمله تحت چند فرض، شاهد تحول بزرگی در دیگر شاخه های مرتبط با این موضوع خواهیم بود.

تحقیقات در بخش پایه‌ی منطق محاسباتی به طور گسترده‌ای بر دیگر بخشهای این علم تاثیر دارند. این تحقیقات عموما به دو بخش تقسیم میشوند:

• تحقیقات در زمینه‌های روشهای استنتاج از قبیل Resolution و …
• تحقیقات در زمینه‌ی پیدا کردن پایه[۱] های مناسب ریاضی برای انجام به صرفه‌ی (از نظر زمانی و حافظه) محاسبات مربوط به منطق محاسباتی.

۲-۱ پایه‌های منطق محاسباتی

روش کلی برای فهمیدن درستی یک جمله این است که از فرضها شروع کرده و در هر مرحله یک جمله درست جدید را با توجه به جملات قبلی و استفاده از قواعد استنتاج تولید کنیم. (یعنی جملات  درست را لیست میکنیم.) این کار ادامه پیدا میکند تا وقتی که به جمله مورد سوال یا نقیض آن برسیم.

قسمت دیگری که مورد توجه است، یکی سازی[۲] است. به طور مثال دو جمله $x:f(x) و $y:f(y) را در نظر بگیرید. واضح است که درستی این دو جمله یکسان است. به طور کلی هر جمله را به طریقه های ظاهرا متفاوت بسیار زیادی میتوان نوشت که همگی یک معنای واحد داشته باشند. (در همین مثال به جای x از تمام متغیرها میتوان استفاده کرد. به صورت معمولی لااقل _­۰N متغیر داریم.) بدین منظور تحقیقات زیادی بر روی روشهای کارا برای یکی سازی جملات منطقی انجام شده است.

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

Resolution Propositional

در این روش تمام جمله ها به صورت clausal form هستند. برای تبدیل یک جمله به این فرم ابتدا جمله را به صورت نرمال عطفی CNF تبدیل میکنیم.

¬(g Ù ( r → f))       ──CNFà      (¬g Ú r) Ù (¬g Ù ¬f)

و سپس نتیجه را به تعدادی مجموعه تبدیل میکنیم، مجموعه ای از مجموعه ها که هر عضو آن اعضای یکی از پرانتزهاست:

(¬g Ú r) Ù (¬g Ù ¬f)       ──Clausal Formà      {¬g, r}, {¬g, ¬f}

این کار یک روش نسبتا خوب برای Unification است.  برای انجام استنتاج بر اساس این قاعده عمل میکنیم:

میدانیم که

(p Ú q) Ù (¬p Ú r) Þ (q Ú r)

میتوان نشان داد که استفاده از این رابطه به عنوان تنها قاعده استنتاج برای استنتاج کافی است. این رابطه در clausal form به این شکل تبدیل میشود:

{p, q}

{¬p, r}

————

{q, r}

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

{¬p, q}

{p}

————

{q}

(این معادل با قاعده Modus Ponens است.)

{p}

{¬p}

————

{}

(تناقض!)

۲-۲ پایه‌ی ریاضی

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

۳ کاربردهای منطق محاسباتی

منطق محاسباتی امروزه به طور گسترده‌ای جهت حل مسایل مهندسی در حال استفاده است و این استفاده با سرعت زیادی در حال گسترش است. زمینه‌های مهمی که امروزه از منطق محاسباتی در آنها استفاده میشود عبارتند از:

• Database Systems

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

• Software Analysis

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

• Hardware Engineering

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

• Automated Theorem Proving

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

۳-۱ STRIPS

یکی از مهمترین مسایل در علم روباتیک برنامه ریزی حرکت روبات[۳] است. روباتی را در نظر بگیرید که دارای توانایی‌های متعارف حرکتی است و قادر است با دستهای خود اقدام به جابجا کردن اشیا نماید، همچنین به وسیله چشم الکترونیکی خود میتواند اطلاعات تصویری از جهان پیرامون خود دریافت کند و آنها را تجزیه و تحلیل کند. این ویژگیها برای یک روبات همگی ویژگیهایی مکانیکی محسوب میشوند. روباتی با این ویژگیها مهمترین کاری که باید بتواند انجام دهد این است که بتواند به طریقه‌ای مفید از قابلیتهای مکانیکی خود استفاده کند.

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

STRIPS عضو یک رده از حل‌کننده‌های مسایل[۴] است که در فضای مدلهای جهان[۵] برای یافتن مدلی که در آن یک هدف داده شده یافت شود، جستجو میکنند. برای هر مدل جهان فرض میکنیم یک  مجموعه از عملگرهای قابل اعمال به جهان وجود دارند. هر عملگر مدل جهان را عوض میکند، به این ترتیب با استفاده از عملگرهای مختلف میتوانیم از یک مدل به مدلهای مختلفی برویم. وظیفه‌ی حل‌کننده مساله این است که دنباله‌ای از عملگرها را پیدا کند که توسط آنها بتوان از یک مدل ابتدایی به مدلی انتهایی رسید که هدف داده شده را ارضا کند.

این چارچوب برای حل مسایل در مورد بسیاری از مسایل هوش‌مصنوعی قابل اعمال است، اما هدف ما در اینجا حل مسایلی که یک ربات با آنها مواجه میشود است. مدل جهان این گونه از مسایل بسیار گسترده و پیچیده است. برای مقایسه مسایل مرتبط با حل پازل را در نظر بگیرید. مدل یک پازل را میتوان به سادگی در یک لیست  یا ماتریس نگه داشت. اما در مورد یک ربات مدل ما از جهان شامل حجم بزرگی از اطلاعات مثل مکان ربات، مکان و خصوصیات اشیا، فضاهای باز و دیوارها و … میباشد. بدین ترتیب یکی از بزرگترین مسایل دراین مورد نحوه نگه داری مدل جهان است. در STRIPS مدل جهان در یک مجموعه از فرمولهای خوش شکل ریخت(wff)[6]  در زبان منطق مرتبه اول، نگه داری میشود.

عملگر[۷]ها عناصر اصلی برای پیدا کردن جواب هستند. هر عملگر متناظر با یک روال کاری[۸] است. فرق این دو این است که عملگرها هنگام برنامه ریزی استفاده میشوند ولی روالهای کاری وقتی استفاده میشوند که ربات میخواهد جواب پیدا شده را به صورت فیزیکی انجام دهد. (یعنی یک عملگر در جهان منطقی معادل با یک روال کلری در جهان واقعی است.)

سوال بعدی این است که یک عملگر مدل جهان را چگونه تغییر میدهد؟ در STRIPS این کار از طریق یک لیست اضافه[۹] و یک لیست حذف [۱۰] انجام میشود. همچنین هر عملگر تعدادی شرط مقدماتی [۱۱] برای انجام شدن دارد.

فایل کامل مقاله آشنایی با منطق محاسباتی ۳۹ صفحه بصورت ورد word همراه با منابع و ماخذ می باشد. 

در تمامی ساعات شبانه روز >> پرداخت آنلاین و دانلود آنی فایل پس از پرداخت.