تحقیق مقاله منطق محاسباتی

خلاصه

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

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

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

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

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

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

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

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

تحقیقات در زمینه‌های روشهای استنتاج از قبیل Resolution و ...

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

2-1 پایه‌های منطق محاسباتی:

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

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

برای تولید جملات جدید با توجه به قواعد استنتاج راه های زیادی پیشنهاد شده اند. یکی از محبوبترین راههای پیشنهاد شده به 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}

————

{}

(تناقض!)

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

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

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

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

Database Systems

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

Software Analysis

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