Введение. 
Метод резолюций и его применение в алгебре высказываний и алгебре предикатов

На протяжении многих тысячелетий человечество занимается накоплением, обработкой и передачей знаний. Для этих целей непрерывно изобретаются новые средства и совершенствуются старые: речь, письменность, почта, телеграф, телефон и т. д. Большую роль в технологии обработки знаний сыграло появление компьютеров.

В октябре 1981 года Японское министерство международной торговли и промышленности объявило о создании исследовательской организации — Института по разработке методов создания компьютеров нового поколения (Institute for New Generation Computer Technology Research Center). Целью данного проекта было создание систем обработки информации, базирующихся на знаниях. Предполагалось, что эти системы будут обеспечивать простоту управления за счет возможности общения с пользователями при помощи естественного языка. Эти системы должны были самообучаться, использовать накапливаемые в памяти знания для решения различного рода задач, предоставлять пользователям экспертные консультации, причем от пользователя не требовалось быть специалистом в информатике. Предполагалось, что человек сможет использовать ЭВМ пятого поколения так же легко, как любые бытовые электроприборы типа телевизора, магнитофона и пылесоса. Вскоре вслед за японским стартовали американский и европейский проекты.

Появление таких систем могло бы изменить технологии за счет использования баз знаний и экспертных систем. Основная суть качественного перехода к пятому поколению ЭВМ заключалась в переходе от обработки данных к обработке знаний. Японцы надеялись, что им удастся не подстраивать мышление человека под принципы функционирования компьютеров, а приблизить работу компьютера к тому, как мыслит человек, отойдя при этом от фон неймановской архитектуры компьютеров. В 1991 году предполагалось создать первый прототип компьютеров пятого поколения.

Теперь уже понятно, что поставленные цели в полной мере так и не были достигнуты, однако этот проект послужил импульсом к развитию нового витка исследований в области искусственного интеллекта и вызвал взрыв интереса к логическому программированию. Так как для эффективной реализации традиционная фон неймановская архитектура не подходила, были созданы специализированные компьютеры логического программирования PSI и PIM.

В качестве основной методологии разработки программных средств для проекта ЭВМ пятого поколения было избрано логическое программирование. Логическое программирование основано на таком разделе математической логики, как исчисление предикатов. Точнее, его базис составляет процедура доказательства теорем методом резолюции для хорновских дизъюнктов.

Этот метод, разработанный американским математиком Дж. Робинсоном в 1965 году, способствовал значительному прогрессу в автоматическом доказательстве теорем. Корни этого метода лежат в исследованиях известного французского логика Ж. Эрбрана, который в 1930 году доказал очень важную теорему, послужившую основой для предложенного им механического метода доказательства теорем. Но при отсутствии в то время вычислительных машин алгоритм Эрбрана оказался весьма трудоёмким для ручных вычислений и не получил практического применения.

С появлением вычислительных машин интерес к механическому доказательству теорем резко возрос. В 1960 году эрбрановский алгоритм был реализован на ЭВМ, были сделаны попытки его усовершенствования, но полученные программы были всё же мало эффективны. Значительный прогресс в деле автоматического доказательства теорем начался с открытия Робинсоном в 1965 году принципа резолюций.

И сейчас в связи с быстрым развитием методов и средств логического программирования и фундаментальным значением, которое приобретает математическая логика для дальнейшего развития информатики в целом, большое внимание следует уделить методу резолюций, который лежит в основе логического программирования — относительно нового направления в программировании, с помощью которого решается большинство задач искусственного интеллекта.

Целью данной курсовой работы является изучение метода резолюций и применение его в логике высказываний и логике предикатов. Для этого подробно рассмотрим суть метода для логики высказываний и логики первого порядка. Остановимся на основных стратегиях, применяемых при решении задач. И, наконец, применим наш метод на практике, решив различные типы задач на данную тему.