استدلال خودکار به رویکردی از علوم کامپیوتر و منطق ریاضی اشاره دارد که مربوط به درک جنبه‌های مختلف استدلال است. استدلال خودکار منجر به تولید برنامه‌هایی میشود که کمک می‌کند کامپیوترها به‌طور کامل و مستقل توانایی استدلال داشته باشند.
در حال حاضر توسعه یافته‌ترین زیرشاخه این علم اثبات قضیه خودکار و بررسی برهان خودکار هستند. نرم‌افزارهای اثبات قضیه خودکار قادرند برخی مسائل و قضایای ریاضی را اثبات نمایند و حتی در مواردی موفق به کشف اثبات‌های کوتاه تر برای برخی از قضایای ریاضی شده‌اند.
استدلال چیست؟
قبل از آن‌که به تعریف این دو مفهوم بپردازیم، اجازه دهید ابتدا به بررسی این موضوع بپردازیم که استدلال چیست؟ استدلال (Reasoning)، ترکیب قانون‌مند قضیه(های) معلوم برای رسیدن به قضیه(های) تازه است.
در استدلال، ذهن بین چند قضیه، ارتباط برقرار می‌کند تا از پیوند آن‌ها، نتیجه زاده شود و به این‌ترتیب نسبتی مشکوک و مبهم به نسبتی یقینی تبدیل شود به عبارتی دیگر به تجمیع تصدیقات (به جملات خبری گفته میشود که بر سلب یا ایجاب مطلبی دیگر امر دارد. مانند: جیوه فلز است. انسان حیوان نیست).
استدلال خودکار چیست؟
استدلال خودکار معمولاً شاخه‌ای از هوش مصنوعی است، اما به مقدار زیادی به علوم رایانه نظری و حتی فلسفه مربوط است. بسیاری بر این باور هستند که گردهمایی Cornell Summer در سال ۱۹۵۷میلادی که میان جمعی از منطق‌دانان و دانشمندان علم رایانه برگزار شده، باعث پایه‌گذاری استدلال خودکار است.
این علم در دهه هشتاد و نود مورد توجه بسیار قرار گرفت. در سال ۲۰۰۵شرکت مایکروسافت در بسیاری از پروژه‌های داخلی خود شروع به استفاده از این استدلال، در تشخیص درستی محصولات خود کرد. توسعه منطق نقش به سزایی در پیشرفت استدلال خودکار داشته‌است.
یک اثبات درست، اثباتی‌ست که در آن هر استنتاجی که استفاده میشود، اصل آن بر پایه اصول منطق باشد. همه مراحل اثبات باید به درستی نشان داده شده و پذیرش آن بر اساس شهود نباشد. این باعث کم شدن خطا در اثبات میشود.
مشکلی که یک برنامه استدلال خودکار ملزم به حل آن است، دارای دو بخش است. اول فرض مسئله که شامل داده‌هایی‌ست که در مواجهه با مسئله به دست می‌آید.
بخش دوم هم نتیجه‌ای است که از استدلال داده‌ها به دست می‌آید. حل مسئله به معنای اثبات حکم آن از روی فرض، بر پایهٔ اصول استتاجی است که در بدنهٔ برنامهٔ استدلال وجود دارد. فرآیند حل مسئله زمانی پایان می‌یابد که اثبات مسئله موجود پیدا شده باشد یا برنامه عدم وجود اثبات را تشخیص داده باشد.
Logic Theorist (LT) اولین برنامه استدلال خودکار بود که در سال ۱۹۵۶با عنوان «شبیه‌سازی استدلال انسان» برای اثبات تئوری‌ها ارائه شد و برای ۵۲قضیه از کتاب مبادی ریاضیات اجرا شد که در ۳۸مورد از آن‌ها به درستی عمل کرد و توانست آن‌ها را اثبات کند.
علاوه بر این، این برنامه توانست برای یکی از قضایا اثباتی ارائه دهد که از اثبات ارائه شده در کتاب به مراتب بهتر و کوتاه‌تر بود. نویسندگان این کتاب پس از آن نوشته‌اند: “در دنیای کنونی، ماشین‌ها فکر می‌کنند. ماشین‌ها یادمی‌گیرند و می‌سازند. این توانایی آن‌ها به سرعت رو به رشد است، تا جایی که در آینده بتوانند به اندازه‌ی یک انسان در حل مسائل پیشرفت کنند.”
استدلال خودکار چه کاربردهایی دارد؟
برنامه‌نویسی منطقی: برنامه‌نویسی منطقی که با عمدتاً با زبان Prolog شناخته میشود، مهم‌ترین کاربرد از استدلال خودکار است. در سال ۱۹۷۰دانشمندان پی‌بردند که از منطق می‌توان به عنوان یک زبان برنامه‌نویسی استفاده کرد.
تایید سخت‌افزارها: با پیشرفت استدلال خودکار، در حوزهٔ صنعت از این تکنولوژی بهره می‌برند. از جمله استفاده آن برای تأیید کارکرد سیستم‌های سخت‌افزاری است. از آنجا که وجود مشکلات کوچک در اینگونه سیستم‌ها گاه می‌تواند برای شرکت‌های سازنده خسارت‌های فراوانی به بار آورد، تأیید درستی آن پیش از عرضه بسیار برای شرکت‌ها مهم است.
از طرفی تست کردن تراشه‌ها راه مناسبی به نظر نمی‌رسد. اما با استفاده از استدلال خودکار و با اثبات‌های ریاضیاتی، نشان می‌دهند که سیستم به خوبی وظیفه مدنظر را انجام می‌دهد.
هوش مصنوعی: استدلال خودکار در حوزه هوش مصنوعی کاربرد فراوان دارد. در واقع می‌توان گفت استدلال خودکار قلب هوش مصنوعی است. زیرا در این حوزه، رایانش برابر است با استنتاج و حل مسئله.
گام‌هایی که در استنتاج مسئله طی میشود در نهایت منجر به رسیدن به هدف معین میشود. پایهٔ ایجاد یک محصول دارای هوش مصنوعی، جمع‌آوری استدلال‌های «اگر – آنگاه» مربوط به جهان اطراف محصول است.
استدلال استقرایی چیست؟
استقرا (Induction) یا استدلال استقرائی (Inductive reasoning) نوعی استدلال است که مقدمات آن از نتیجه به صورت محتمل پشتیبانی می‌کنند. در مقابل استدلال قیاسی است که مقدمات به صورت قطعی از نتیجه حمایت می‌کنند. در منطق کلاسیک استدلال استقرایی را استدلال از جزء به کل تعریف می‌کردند که در منطق جدید این تعریف پذیرفته نیست.
بعضی انواع استقرا تعمیم، استدلال علی، استدلال بر مبنای تمثیل و پیش‌بینی نام دارند. فرایند استقراء از مشاهدات جزئی شروع شده و استنتاج نتایج تعمیم داده میشود.
هر استدلال مدعی است که مقدمات آن زمینه درستی نتیجه آن استدلال را فراهم می‌سازند و در واقع حضور همین ادعا هست که نشان دهنده وجود یک استدلال است. یک استدلال استنتاجی مدعی است که مقدمات آن نتیجه را به‌طور قطعی پشتیبانی می‌کند. به عکس یک استدلال استقرایی چنین ادعایی ندارد.
اگر قضاوت ما از تفسیر یک متن استدلالی اینگونه باشد که چنین ادعایی به قطع وجود دارد، آنگاه برداشت ما از آن متن یک استدلال استنتاجی است. اگر چنین قضاوتی نداشته باشیم، برداشت ما از آن متن یک استدلال استقرایی است. از آنجا که در هر استدلال چنین قطعیتی (به‌طور ضمنی یا صریح) ادعا میشود یا نمی‌شود، بنابراین هر استدلال استنتاجی یا استقرایی خواهد بود.
استدلال کل به جزء یا استدلال قیاسی (deductive reasoning) یکی از دو استدلال معروف در منطق (استدلال کل به جزء و استدلال جزء به کل {the deductive and inductive approaches}) است.
استدلال کل به جزء هنگامی است که در استدلال از یک نظریه (تئوری) کلی استفاده کنیم و به فرضیه یا فرضیه‌های جزئی برسیم. در پژوهش ها، زمانی که پژوهشگر از نظریه استفاده می‌کند و فرضیه می‌سازد و برای ازمون فرضیه‌ها داده جمع‌آوری می‌کند و نتیجه میگیرد می گوییم پژوهشگر از روش استدلال کل به جزء استفاده کرده‌است.
روش استدلال جزء به کل (inductive approaches) بر عکس این روش می‌باشد یعنی پژوهشگر داده جمع‌آوری می‌کند و الگو بین داده‌ها و متغیرها کشف می‌کند سپس فرضیه می‌سازد و فرضیه را آزمون می‌کند و در نهایت نظریه می‌دهد. روش‌های جز به کل و کل به جز از دو روش مهم در پژوهش می‌باشد (the deductive and inductive methods).
استقرا تام
استقرا تام در جایی است که افراد مورد نظر، یعنی نمونه‌های جزئی که می‌خواهیم از آن‌ها نتیجه‌گیری کنیم، به تعدادی باشند که بتوانیم همه آن‌ها را بررسی کنیم، یعنی افراد و نمونه‌ها، محدود و معدود باشند و هر یک جداجدا مورد بررسی قرار گرفته باشند و پس از بررسی همه آن‌ها، حکم کلی صادر شود. این حکم کلی در مورد همهٔ آن‌ها صادق است، زیرا تک تک آن‌ها مورد بررسی قرار گرفته و مشمول این حکم بوده‌اند.
استقرا ناقص
این استقرا در صورتی است که همهٔ افراد مورد نظر بررسی نشده باشند. به این صورت که ما در تعدادی از آن‌ها صفتی معین بیابیم و سپس حکم کنیم که همه افراد آن موضوع دارای آن صفت هستند. مثال زیر، ویژگی این روش را نشان می‌دهد:
- همه انسان‌هایی که تاکنون دیده‌ام می‌میرند.
- سقراط انسان است.
- بنابراین: سقراط خواهد مرد.
پیش فرض نخست بیان می‌کند که همه موجودات قرار گرفته زیر نام و عنوان «انسان» که تاکنون مورد مشاهدهٔ فرد مدعی قرار گرفته‌اند می‌میرند.
عبارت دوم بیان می‌کند: سقراط هم زیر عنوان یک «انسان» قرار دارد. در نتیجه سقراط بالاخره می‌میرد، زیرا او نیز به عنوان یک انسان خواهد مرد، چون که عنوان «انسان» به او نسبت داده شده و این ویژگی او را نیز شامل میشود.
روش استقرایی ـ قیاسی
روش استقرایی ـ قیاسی روشی است که از زمان ارسطو باب شده، و در سیر تحولی خود در عهد رنسانس در علوم مختلف تجربی آن را نقد و بررسی کرده‌اند. در مجموع می‌توان گفت دانشمندان مختلف اصل روش استقرایی ـ قیاسی را پذیرفته بودند، اما کسانی مانند بیکن در قرن شانزدهم و هفدهم در کیفیت شرایط و اصول موضوعه اش مجادلاتی با روش ارسطویی داشته‌اند که این مجادلات به تصحیح روش ارسطویی می‌انجامید، ولی در کنار این روش، روش استقرایی محض، که مورد تأیید کسانی چون دونس اسکوتس، اکام، هیوم و هرشل بود، در قرن نوزدهم به همت جان استوارت میل به‌طور فزاینده ای تبلیغ و ترویج شد. میل مدعی بود که از راه استقرای صرف و بدون کاربست روش قیاسی می‌توان به ضرورت و علیت پدیده‌ها دست یافت. روش استقرایی محض در قرن بیستم به مکتب اصالت تجربه انجامید. این مکتب به‌طور کلی منکر هرگونه معرفت پیشین و غیر حسی است.
استدلال موردی
در این میان است استدلال دیگری نیز وجود دارد که به تدریج به دنیای هوش مصنوعی در حال ورود است. این رویکرد استدلال موردی نام دارد. استنتاج موردی (Case-based reasoning) که به‌طور گسترده‌ای تفسیر شده‌است، در واقع فرایند حل مشکلات جدید بر اساس راه حل‌های مشکلات مشابه در گذشته‌است.
یک مکانیک خودرو معمولاً موتور را با به یاد آوردن ماشینی دیگر تعمیر می‌کند که علایم مشابهی با هم دارند، پس در این صورت از استدلال مبتنی بر مورد استفاده می‌کند. وکیلی که از یک پیامد خاص در یک محاکمه براساس سوابق قانونی یا قاضی حمایت می‌کندکه قانون موردی را ایجاد می‌کند، از استدلال مبتنی بر مورد استفاده می‌کند.
استدلال مبتنی بر مورد تنها یک روش قدرتمند برای استدلال خودکار نیست بلکه یک روش فراگیر در حل مسائل روزمره است. این دیدگاه مربوط به نظریه پروتوتایپ است که در علوم شناختی کشف شده.
روش استدلال مبتنی بر مورد بر اساس استفاده از پاسخ مسائل قبلی برای حل مسائل مشابه جدید شکل گرفته است. CBR بعنوان روشی شناخته میشود که از نحوۀ رفتار انسانها در برخورد با مسائل جدید الگوبرداری کرده است؛
به این ترتیب که از تجربیات کسب شده در حل مسائل گذشته بعنوان راهنمائی برای حل مسائل جدید بهره میبرد. حل مساله به روش CBR در یک چرخه انجام میگیرد و در برگیرندۀ چهار عمل عمده به شرح زیر است:
- بازیابی” مورد” مشابه با مسالۀ جدید
- استفاده از پاسخ مسالۀ مشابه بازیابی شده برای تهیه پاسخ پیشنهادی برای مسالۀ جدید
- بازبینی در پاسخ پیشنهادی در صورت وجود مغایرت در شرایط مسالۀ جدید و مسالۀ بازیابی شده
- نگهداری مورد جدید (مساله جدید و پاسخ آن) برای استفاده در آینده
در نگاه اول، CBR ممکن است شبیه الگوریتم‌های القایی قانون از یادگیری ماشین باشد. مانند الگوریتم القایی قانون، CBR هم با مجموعه ای از مسائل و مثال‌های آموزشی شروع میشود.
این تعاریف از این نمونه‌ها، با شناسایی نقاط مشترک بین پرونده بازیابی شده و مسئله هدف، شکل میگیرد. به‌طور مثال اگر روش ساده پنکیک درست کردن به روشی برای پنکیک بلوبری تعمیم داده شود، شرایطی ایجاد می‌کند که از روش‌های خاصی برای پخت آن استفاده شود. در واقع تفاوت بین تعمیم ضمنی در CBR و تعمیم در القای قاعده زمانی است.
الگوریتم القایی قانون، تعمیم مجموعه‌های آزمایشی نمونه‌ها را قبل از شناخت مسئله هدف ترسیم می‌کند. به عنوان مثال اگر از این الگوریتم برای آموزش انواع پنکیک‌ها مانند پنکیک هلندی یا پنکیک موز استفاده شود، قبل از هر کاری باید قواعد و نوع پخت پنکیک‌های ساده و نکات آن را یاد داد.
دشواری الگوریتم القایی قانون در پیش‌بینی جهت‌های مختلف است که در آن باید تلاش شود مثال‌های آموزشی تعمیم پیدا کنند. در مثال پنکیک، CBR مسئله هدف را با استفاده از پنکیک زغال اخته بررسی کرده‌است. پس می‌تواند موارد خود را دقیقاً همان‌طور که مورد نیاز برای پوشش وضعیت جدی است، تعمیم دهد.
در قانون، اغلب مواردی از CBR به دادگاه منتقل میشود و محدودیت‌های دلایل قانونی را به رسمیت می‌شناسد که این موارد عبارتند از: تأخیر محدود، دانش مجدود درباره آینده، محدودیت مذاکره و….
