استدلال خودکار
استدلال خودکار (به انگلیسی: automated reasoning) حوزه‌ای از علوم کامپیوتر و منطق ریاضی است که مربوط به درک جنبه‌های مختلف از استدلال است. استدلال خودکار منجر به تولید برنامه‌هایی می‌شود که کمک می‌کند کامپیوترها به‌طور کامل و مستقل توانایی استدلال داشته باشند. با این تعریف، استدلال خودکار معمولاً شاخه‌ای از هوش مصنوعی به‌شمار می‌آید، اما به مقدار زیادی به علوم رایانه نظری و حتی فلسفه مربوط است.
در حال حاضر توسعه‌یافته‌ترین زیرشاخه این علم اثبات قضیه خودکار و بررسی برهان خودکار هستند. نرم‌افزارهای اثبات قضیه خودکار قادرند برخی مسائل و قضایای ریاضی را اثبات نمایند و حتی در مواردی موفق به کشف اثبات‌های کوتاه تر برای برخی از قضایای ریاضی شده‌اند.
تعریف
ویرایشمشکلی که یک برنامهٔ استدلال خودکار ملزم به حل آن است، دارای دو بخش است. اول فرض مسئله که شامل داده‌هایی‌ست که در مواجهه با مسئله به دست می‌آید. بخش دوم هم نتیجه‌ای است که از استدلال داده‌ها به دست می‌آید. حل مسئله به معنای اثبات حکم آن از روی فرض، بر پایهٔ اصول استنتاجی است که در بدنهٔ برنامهٔ استدلال وجود دارد. فرآیند حل مسئله زمانی پایان می‌یابد که اثبات مسئلهٔ موجود پیدا شده باشد یا برنامه عدم وجود اثبات را تشخیص داده باشد.
تاریخچه
ویرایشتوسعهٔ منطق نقش به سزایی در پیشرفت استدلال خودکار داشته‌است. یک اثبات درست، اثباتی‌ست که در آن هر استنتاجی که استفاده می‌شود، اصل آن بر پایهٔ اصول منطق باشد. همهٔ مراحل اثبات باید به درستی نشان داده شده و پذیرش آن بر اساس شهود نباشد. این باعث کم شدن خطا در اثبات می‌شود.
بسیاری گفته‌اند که گردهمایی Cornell Summer در سال ۱۹۵۷ میلادی که میان جمعی از منطق دانان و دانشمندان علم رایانه برگزار شده بود، باعث پایه‌گذاری استدلال خودکار است. این علم در دههٔ هشتاد و نود مورد توجه بسیار قرار گرفت. در سال ۲۰۰۵ شرکت مایکروسافت در بسیاری از پروژه‌های داخلی خود شروع به استفاده از این استدلال، در تشخیص درستی محصولات خود کرد.
Logic Theorist (LT) اولین برنامهٔ استدلال خودکار بود که در سال ۱۹۵۶ با عنوان «شبیه‌سازی استدلال انسان» برای اثبات تئوری‌ها ارائه شد و برای ۵۲ قضیه از کتاب مبادی ریاضیات اجرا شد که در ۳۸ مورد از آن‌ها به درستی عمل کرد و توانست آن‌ها را اثبات کند. علاوه بر این، این برنامه توانست برای یکی از قضایا اثباتی ارائه دهد که از اثبات ارائه شده در کتاب به مراتب بهتر و کوتاه‌تر بود. نویسندگان این کتاب پس از آن نوشته‌اند: "در دنیای کنونی، ماشین‌ها فکر می‌کنند. ماشین‌ها یادمی‌گیرند و می‌سازند. این توانایی آن‌ها به سرعت رو به رشد است، تا جایی که در آینده بتوانند به اندازه‌ی یک انسان در حل مسائل پیشرفت کنند."
کاربردها
ویرایشبرنامهنویسی منطقی: برنامه‌نویسی منطقی که با عمدتاً با زبان Prolog شناخته می‌شود، مهم‌ترین کاربرد از استدلال خودکار است. در سال ۱۹۷۰ دانشمندان پی‌بردند که از منطق می‌توان به عنوان یک زبان برنامه‌نویسی استفاده کرد.
تایید سخت‌افزارها: با پیشرفت استدلال خودکار، در حوزهٔ صنعت از این تکنولوژی بهره می‌برند. از جمله استفاده آن برای تأیید کارکرد سیستم‌های سخت‌افزاری است. از آنجا که وجود مشکلات کوچک در این‌گونه سیستم‌ها گاه می‌تواند برای شرکت‌های سازنده خسارت‌های فراوانی به بار آورد، تأیید درستی آن پیش از عرضه بسیار برای شرکت‌ها مهم است. از طرفی تست کردن تراشه‌ها راه مناسبی به نظر نمی‌رسد. اما با استفاده از استدلال خودکار و با اثبات‌های ریاضیاتی، نشان می‌دهند که سیستم به خوبی وظیفهٔ مدنظر را انجام می‌دهد.
هوش مصنوعی: استدلال خودکار در حوزهٔ هوش مصنوعی کاربرد فراوان دارد. در واقع می‌توان گفت استدلال خودکار قلب هوش مصنوعی است. زیرا در این حوزه، رایانش برابر است با استنتاج و حل مسئله. گام‌هایی که در استنتاج مسئله طی می‌شود در نهایت منجر به رسیدن به هدف معین می‌شود. پایهٔ ایجاد یک محصول دارای هوش مصنوعی، جمع‌آوری استدلال‌های «اگر - آنگاه» مربوط به جهان اطراف محصول است.