На головну

Лабораторна робота № 4

  1. Cамостійна робота
  2. Бичачий ціп'як. Систематичне положення, морфологія, цикл розвитку, лабораторна діагностика. Теніаринхозу.
  3. Вивчай робота кардіологічніх кабінетів поліклінік м. С. визначний одиницю спостереження.
  4. ВИМОГИ ДО реферат (МАЛА КУРСОВА РОБОТА) ЗІ спеціальності
  5. Виховна робота в ВНЗ
  6. Вставка формул. Робота з редактором рівнянь Equation Editor
  7. групова робота

Мета роботи:ознайомитися з принципом резолюцій докази істинності логічних висловлювань, навчитися перевіряти істинність логічних міркувань шляхом побудови резолютивної виведення.

ТЕОРЕТИЧНІ ВІДОМОСТІ

Метод резолюцій - це метод докази того, що формула G є логічним наслідком формул F1, F2, ..., Fk. Відзначимо, що завдання про логічному слідстві зводиться до задачі про здійсненності. Дійсно, формула G є логічний наслідок формул F1, F2, ..., Fk тоді і тільки тоді, коли безліч формул {F1, F2, ..., Fk,} Неможливо. Метод резолюцій, якщо говорити більш точно, встановлює нездійсненність. Таким чином, міркування, що є основою методу резолюцій, полягають в наступному: щоб довести, що, необхідно показати, що - тавтологія. Це перша особливість методу. Друга особливість методу полягає в тому, що він оперує не з будь формулами, а з диз'юнкт (або елементарними диз'юнкції).

Введемо кілька визначень.

Визначення 1. Нехай,. Диз'юнкт називається резольвенти диз'юнктів і по змінної і позначається через. Очевидно, що .

Визначення 2. Правилом резолюцій в логіці висловлювань називається наступне правило: з диз'юнктів і виводимо диз'юнкт.

Визначення 3. Нехай - безліч диз'юнктів. Послідовність формул називається резолютивним висновком з Г, Якщо для кожної формули, виконується одна з умов:

1.

2. .

Застосування методу резолюцій засноване на наступному твердженні, яке називається теоремою про повноту методу резолюцій.

Теорема 1.Безліч диз'юнктів Г суперечливо в тому і тільки в тому випадку, коли існує резолютивну висновок з Г, який закінчується нулем.

Приклад 1.Покажемо, що формула G=С є логічним наслідком формул,. Сформуємо множину формул. Необхідно формули і привести до КНФ (формула сама має цю форму), щоб перетворити безліч Т в безліч диз'юнктів.

Тоді безліч диз'юнктів.

Побудуємо можливий резолютивну висновок нуля з S:

1)

2)

3)

4)

5)

6)

Отже, формула G є логічним наслідком формул F1 и F2.

Приклад 2. Перевіримо за допомогою методу резолюцій виводимість. Виводимість даної формули з Г за цим методом слід з суперечливості множини. Наведемо всі формули з Г1 до КНФ:

Таким чином, отримуємо безліч диз'юнктів

.

Побудуємо можливий резолютивну висновок нуля з S:

1)

2)

3)

4)

5)

6)

7)

8)

9)

10)

11)

12)

13)

14)

Отже, формула є логічним наслідком з посилок Г.

ЗАВДАННЯ ДО ЛАБОРАТОРНОЇ РОБОТИ № 3

1) Показати, що формула G - Є логічним наслідком формул за допомогою методу резолюцій (відповідно до Вашого варіанту):

Варіант 1.

Варіант 2.

Варіант 3.

Варіант 4.

Варіант 5.

Варіант 6.

Варіант 7.

Варіант 8.

Варіант 9.

Варіант 10.

2)Написати програму на мові комп'ютерної системи Maple, що реалізує алгоритм методу резолюцій, що дозволяє перевірити здійсненність. Порівняти результат аналітичного рішення з результатом роботи програми.

ВИМОГИ ДО ОФОРМЛЕННЯ ЗВІТУ ПО РОБОТІ

У звіт необхідно включити:

1. мета роботи,

2. умову задачі,

3. аналітичне рішення задачі,

4. лістинг програми з необхідними коментарями,

5. висновок про виконану роботу.

Лабораторна робота № 4



Метод резолюцій в логіці висловлювань | Стислі Відомості з Теорії.
© um.co.ua - учбові матеріали та реферати