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