Задача логического вывода в теории L

- Пропустить и перейти к материалам
- Пропустить и перейти к главной навигации
- Пропустить и перейти к первому столбцу
- Пропустить и перейти ко второму столбцу

# Библиотека учебных материалов

для студентов

Home Примеры решения задач Дискретная математика Задача логического вывода в теории L

## Задача логического вывода в теории L

Проверить выполнение логического вывода 4 способами: с помощью формального вывода, неформального вывода, метода резолюций, построения логической программы:

Ни один муж, дарящий жене новые платья, не может быть несговорчивым. Аккуратный муж всегда возвращается домой к чаю. Жене нелегко содержать в порядке одежду мужа, если он имеет обыкновение вешать свою шляпу на газовый рожок. Хороший муж всегда дарит своей жене новые платья. Ни один муж не может не быть несговорчивым, если жена не следит за его одеждой. Неаккуратный муж всегда вешает свою шляпу на газовый рожок. Вывод: хороший муж всегда возвращается домой к чаю

Решение

Формализация

Предикаты

- х дарит жене платья

- х сговорчивый

- х возвращается домой к чаю

- х аккуратный

- жена х содержит в порядке его одежду

- х вешает одежду на газовый рожок

- х является хорошим

Формализуем посылки

Ни один муж, дарящий жене новые платья, не может быть несговорчивым

Аккуратный муж всегда возвращается домой к чаю

Жене нелегко содержать в порядке одежду мужа, если он имеет обыкновение вешать свою шляпу на газовый рожок

Хороший муж всегда дарит своей жене новые платья

Ни один муж не может не быть несговорчивым, если жена не следит за его одеждой

Неаккуратный муж всегда вешает свою шляпу на газовый рожок.

Вывод: хороший муж всегда возвращается домой к чаю

Формальный вывод

1.

2.

3.

4.

5.

6.

7. пронесение отрицания через квантор (1)

8. определение (7)

9. УК (8)

10. УК(2)

11. УК(3)

12. УК(4)

13. УК(5)

14. УК(6)

15. сил (12,9)

16. сил(14,11)

17. контр(16)

18. сил(17,10)

19. контр(13)

20. сил(15,19)

21. сил(20, 18)

22. Gen(21)

Неформальный вывод

Предположим, что посылки истинны, а вывод ложный:

Поскольку , то найдется такое а, что

Поскольку

и , то

Поскольку

и , то

Поскольку

и , то

Поскольку

и то

Поскольку

и , то

Поскольку

и , то

Однако ранее было доказано что . Таким образом, наше предположение неверно и логическое следование выполняется

Метод резолюций

Составляем множество дизъюнктов

1.

2.

3.

4.

5.

6.

Отрицание от вывода

,

1.

2.

3.

4.

5.

6.

7.

8.

9. P(a) {a/x} рез(7,4)

10. {a/x} рез(9,1)

11. {a/x} рез (2,8)

12. {a/x} рез (6,11)

13. {a/x} рез (12,3)

14. {a/x} рез(13, 5)

15. рез(10,14)

Получение пустого дизъюнкта говорит о том, что логическое следование выполняется

Построение логической программы

Predicates

- х дарит жене платья

- х сговорчивый

- х возвращается домой к чаю

- х аккуратный

- жена х содержит в порядке его одежду

- х вешает одежду на газовый рожок

- х является хорошим

Clauses

Goal

? – not

|

{a/x}

|

|

{a/x}

|

|

{a/x}

|

|

{a/x}

|

|

{a/x}

|

|

{a/x}

|

|

|