Кіріспе
Компьютерлік ғылым мен логиканың кіші саласы Компьютерлік ғылымда, әсіресе білімді бейнелеу мен ойлау және металологияда, автоматтандырылған ойлау саласы ойлаудың әртүрлі аспектілерін түсінуге арналған. Автоматты ойлауды зерттеу компьютерлерге толық немесе толықтай автоматты түрде ойлауға мүмкіндік беретін компьютерлік бағдарламаларды жасауға көмектеседі. Автоматтандырылған ойлау жасанды интеллекттің кіші саласы болып саналатынымен, оның теориялық компьютерлік ғылым мен философиямен байланысы бар. Автоматтандырылған ойлаудың ең дамыған кіші салалары - теоремаларды автоматтандырылған дәлелдеу (және интерактивті теоремаларды дәлелдеудің аз автоматтандырылған, бірақ прагматикалық кіші саласы) және автоматтандырылған дәлелдеуді тексеру (белгілі болжамдар бойынша дұрыс ойлауды кепілдік беру ретінде қарастырылады). Индукция мен абдукцияны қолдана отырып, аналогия арқылы ойлау бойынша да ауқымды жұмыстар жүргізілді. Басқа маңызды тақырыптарға белгісіздік жағдайындағы ойлау және монотонды емес ойлау жатады. Белгісіздік өрісінің маңызды бөлігі - дәлелдеу, онда стандартты автоматтандырылған шегерімге қосымша минималдылық пен сәйкестік шектеулері қолданылады. Джон Поллоктың OSCAR жүйесі - автоматтандырылған теорема провайдерінен гөрі ерекше автоматтандырылған аргументациялық жүйенің үлгісі. Автоматтандырылған ойлаудың құралдары мен әдістері классикалық логика мен калькульді, тұйық логиканы, Байестік тұжырымдауды, максималды энтропиямен ойлауды және көптеген формалды емес арнайы әдістерді қамтиды.
In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub field of artificial intelligence, it also has connections with theoretical computer science and philosophy. The most developed subareas of automated reasoning are automated theorem proving (and the less automated but more pragmatic subfield of interactive theorem proving) and automated proof checking (viewed as guaranteed correct reasoning under fixed assumptions). Extensive work has also been done in reasoning by analogy using induction and abduction. Other important topics include reasoning under uncertainty and non monotonic reasoning. An important part of the uncertainty field is that of argumentation, where further constraints of minimality and consistency are applied on top of the more standard automated deduction. John Pollock's OSCAR system is an example of an automated argumentation system that is more specific than being just an automated theorem prover. Tools and techniques of automated reasoning include the classical logics and calculi, fuzzy logic, Bayesian inference, reasoning with maximal entropy and many less formal ad hoc techniques.
Қолданбалар
Автоматтандырылған ойлау әдетте теорема дәлелдегіштерді құру үшін қолданылады. Алайда, теоремаларды дәлелдеушілер тиімді болу үшін кейбір адам басшылығын қажет етеді, сондықтан олар дәлелдеуші көмекші ретінде біліктілік алады. Кейбір жағдайларда мұндай дәлелдеушілер теореманы дәлелдеудің жаңа тәсілдерін ойлап тапты. Логикалық теоретик - бұған жақсы мысал. Бағдарлама Principia Mathematica теоремаларының бірінің дәлелін ұсынды, ол Уайтхед пен Расселдің дәлеліне қарағанда тиімді (көп қадамдарды қажет етеді). Автоматтандырылған ойлау бағдарламалары формальды логика, математика және компьютерлік ғылымдар, логикалық бағдарламалау, бағдарламалық қамтамасыз ету мен аппараттық тексеру, схемалық дизайн және басқа да көптеген мәселелерді шешу үшін қолданылады. ТПТП (Sutcliffe and Suttner 1998) - бұл осындай проблемалардың кітапханасы, ол тұрақты түрде жаңартылып отырады. Сондай-ақ CADE конференциясында жүйелі түрде теоремаларды автоматтандырылған дәлелдеушілер арасында байқау өткізіледі (Pelletier, Sutcliffe and Suttner 2002); байқауға арналған мәселелер TPTP кітапханасынан таңдалады.