Средства разработки приложений
Давайте посмотрим, как можно привести
Давайте посмотрим, как можно привести любую формулу к множеству дизъюнктов, с которым работает метод резолюций. Для этого нам понадобятся некоторые определения нормальных форм.
Говорят, что формула находится в конъюнктивной нормальной форме,если это конъюнкция конечного числа дизъюнктов. Имеет место теорема о том, что для любой бескванторной формулы существует формула, логически эквивалентная исходной и находящаяся в конъюнктивной нормальной форме.
Формула находится в предваренной (или пренексной) нормальной форме, если она представлена в виде Q1x1,...,QnxnA, где Qi — это квантор ∀ или ∃ , а формула A не содержит кванторов. Выражение Q1x1,...,Qnxn называют префиксом, а формулу A — матрицей.
Формула находится в сколемовской нормальной форме, если она находится в предваренной нормальной форме и не содержит кванторов существования.
Forekc.ru
Рефераты, дипломы, курсовые, выпускные и квалификационные работы, диссертации, учебники, учебные пособия, лекции, методические пособия и рекомендации, программы и курсы обучения, публикации из профильных изданий