Искусственный интеллект

Формулы в постановке задачи не должны содержать кванторов существования. Если они все же есть, то, прежде чем решать задачу, от кванторов существования следует избавиться с помощью, например, правила исключения квантора существования или какими-либо другими способами, речь о которых пойдет дальше. Все формулы в постановке задачи должны быть атомами или импликациями, левая часть (посылка) которых является конъюнкцией атомов, а правая (заключение) — либо атомом, либо пустым символом. Такие формулы называют хорновскими формулами. Преобразование произвольных формул логики предикатов в хорновские формулы непростая задача, причем не любую формулу можно преобразовать к такому виду. В нашем примере со средой чудовища кванторов существования, не считая формулы цели, вообще нет, тем не менее, подобное преобразование всех формул невозможно. Например, это нельзя сделать для формул (4.18), (4.19). Рассмотрим, как выполняется указанное преобразование для формул (4.1) — (4.32). Для того чтобы можно было легко сопоставить эти формулы с их преобразованиями, будем последние нумеровать теми же числами, но со звездочкой, комментируя производимые преобразования (если в преобразованиях нет необходимости, то соответствующая формула переписывается без комментариев):