Средства разработки приложений


Лекция из курса Основы программирования на языке Пролог - часть 3


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

Говорят, что формула находится в конъюнктивной нормальной форме,если это конъюнкция конечного числа дизъюнктов. Имеет место теорема о том, что для любой бескванторной формулы существует формула, логически эквивалентная исходной и находящаяся в конъюнктивной нормальной форме.

Формула находится в предваренной (или пренексной) нормальной форме, если она представлена в виде Q1x1,...,QnxnA, где Qi — это квантор или , а формула A не содержит кванторов. Выражение Q1x1,...,Qnxn называют префиксом, а формулу Aматрицей.

Формула находится в сколемовской нормальной форме, если она находится в предваренной нормальной форме и не содержит кванторов существования.




Начало  Назад  Вперед



Книжный магазин