Структуры данных и модели вычислений



         

Некоторые сведения из математической логики


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

(1)

где — предикатные символы соответствующей арности; , — индивидные переменные.

Известно, что по любому предложению в предваренной нормальной форме можно построить так называемое сколемовское предложение . Для этого избавляются от кванторов существования следующим образом. Пусть ( — самое левое вхождение квантора существования в рассматриваемую формулу и перед ним расположены кванторов общности с переменными . Выбираем новый -местный функциональный символ , вхождение удаляем из формулы, а каждое вхождение переменной заменяем термом . Аналогичным образом избавляемся и от других кванторов существования. В результате получим сколемовскую формулу для исходной формулы .

Так, для формулы (1) соответствующая сколемовская формула будет иметь вид

(2)

полученный из (1) заменой на , а

на . Заметим, что если бы было , то переменная заменялась бы на новую константу. Процесс получения сколемовской формулы по заданной формуле называется сколемизацией.

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

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

Равносильность по выполнимости формулы и соответствующей ей сколемовской формулы может быть использована следующим образом. Предположим, мы хотим доказать, что формула является логическим следствием формул и . Это сводится к доказательству невыполнимости формулы

или соответствующей ей сколемовской формулы, что технически осуществить оказывается проще.




Содержание  Назад  Вперед