Методические указания к выполнению расчетно-графической работы по математической логике и теории алгоритмов

21 Для составления программы нахождения заданной формы (задание № 3) необходимо, как обычно, начинать с построения алгоритма программы, выбрав (определив), что является входными данными программы. Здесь можно выбрать различные варианты. Входом программы может быть аналитическое представление функции или результирующий столбец ее таблицы истинности. Для решения задачи № 4 важно сначала записать конъюнкцию посылок и отрицания заключения. Далее находится к.н.ф. и для полученных дизъюнктов применяется метод резолюций. Рассмотрим задачу выяснения будет ли В логическим следствием из ТО есть истинна ли следующая запись: В § 1 главы 3 пособия показано, что эта задача сводится к выяснению невыполнимости формы С=Л1&Л2&... SiAffiS: IB. Найдем для формулы С ее к.н.ф., то есть получим конъюнкцию дизъюнктов: C=Dj&D2&...&Dk. Теперь применяем метод резолюций к множеству полученных дизъюнктов: {Dj,D2,...,Dk}. Если методом резолюций получается пустой дизъюнкт, то заключение логически следует из посылок. Если же пустой дизъюнкт получить нельзя, то заключение не следует из данных посылок. Задание № 5 аналогично заданию № 1, но сложнее, так как используются дополнительно кванторы и предикаты. Здесь нужно обратить внимание, что при использовании квантора всеобщности используется импликация, а для квантора существования - конъюнкция. Попытайтесь воспользоваться следующими известными предложениями и их символьной записью.