Решатель

Основная задача решателя — это преобразование исходного описания задачи или задания на выполнение некоторой программы в рабочую программу для ЭВМ. Математически эта задача сводится к переводу исходного описания в некоторое промежуточное формализованное описание (описание на языке спе­цификаций, в качестве которого чаще всего выступает исчисление предикатов первого порядка или некоторое подмножество формул, допустимых в подобном исчислении). Подобная формализация рассматри­вается как теорема. Доказательство теоремы можно найти в рам­ках формальной системы, все компоненты которой хранятся в ба­зе знаний. Средства вывода входят в решатель. Построенный вы­вод (при положительном результате доказательства) позволяет извлечь из него рабочую программу, нужную пользователю.

Работы по реализации подобных процедур были начаты в СССР довольно давно, раньше, чем в зарубежных странах. Пер­вые системы такого типа ПРИЗ и СПОРА еще не были достаточ­но эффективными, но заложили основу теории и практики построе­ния подобных систем [40]. В последнее время было показано, что в качестве языка, на котором функционирует решатель, можно использовать языки логического программирования, в частно­сти язык ПРОЛОГ. Переход к языкам такого типа резко повышает эффективность процедур автоматического синтеза программ в решателях [41]. Можно предполагать, 'что подобный подход даст возможность строить вполне приемлемые с практической точки зрения решатели в ЭВМ новых поколений.