Основы современных компьютерных технологий



Логические системы - часть 4


  • ?Х(ВЗЛЕТЕЛ(Х) > ВЫП_РЕЙС(Х))
  • ПРОВЕРЕН(ЯК-42)
  • ЗАПРАВЛЕН(ЯК-42)
  • ПРОВЕРЕН(ТУ-134)
  • ЗАПРАВЛЕН(ИЛ-62)
  • ДАНО_РАЗР(ЯК-42)
  • НЕ_НАХ_ВЗП(ЯК-42)
  • Предложения 1-4, хотя и содержат переменную, являются высказываниями - переменная X связана квантором общности V. В дальнейшем квантор писать не будем, так как он присутствует во всех предложениях.

    Чтобы найти, какой из самолетов в момент времени Т выполняет рейс, подготовим запрос вида:

    М? ВЫП_РЕЙС(1),

    где М - множество предложений 1-10. Вывод запроса можно представить следующей последовательностью шагов.

    1шаг.

    Применив к предложению 1 подстановку Х=ЯК-42, получим заключение

    ПРОВЕРЕН(ЯК-42) ? ЗАПРАВЛЕН(ЯК-42) > ГОТОВ(ЯК-42).

    2 шаг.

    Первая посылка: объединив предложения 5 и 6, получим

    ПРОВЕРЕН(ЯК-42) ? ЗАЛРАВЛЕН(ЯК-42).

    Вторая посылка: заключение шага 1:

    ПРОВЕРЕН(ЯК-42) ? ЗАПРАВЛЕН(ЯК-42) > ГОТОВ(ЯК-42).

    Применив правило Modus Ponens

    ?,? > ?
    ?

     

    299

    для ?= ПРОВЕРЕН(ЯК-42) ? ЗАПРАВЛЕН(ЯК-42) и р= ГОТОВ(ЯК-42), получим

    следующее заключение: ГОТОВ(ЯК-42).

    Зшаг.

    Первая посылка: объединив заключение шага 2, предложения 9 и 10, получим:

    ГОТОВ(ЯК-42) ?ДАНО_РАЗР(ЯК-42) ?НЕ_НАХ_ВЗП(ЯК-42).

    Вторая посылка: применив к правилу 2 подстановку Х=ЯК-42, получим

    ГОТОВ(ЯК-42) ? ДАНО_РАЗР(ЯК-42) ? НЕ_НАХ_ВЗП(ЯК-42) > ВЗЛЕТЕЛ(ЯК-42)

    Применив правило Modus Ponens, получим заключение ВЗЛЕТЕЛ(ЯК-42).

    4 шаг.

    Первая посылка: заключение шага 3 - ВЗЛЕТЕЛ(ЯК-42).

    Вторая посылка: применив к правилу 4 подстановку Х=ЯК-42, получим

    ВЗЛЕТЕЛ(ЯК-42) > ВЫП_РЕЙС(ЯК-42).

    Применив правило Modus Ponens, получим заключение ВЫП_РЕЙС(ЯК-42). Таким образом, в момент времени Т рейс выполняет самолет ЯК-42. Остальные подстановки, например Х=ИЛ-62, приводят к тупиковым ситуациям. Логический вывод выполнялся нами в прямом направлении, при этом в процессе вывода трижды использовалось правило заключения.

    300

    292 :: 293 :: 294 :: 295 :: 296 :: 297 :: 298 :: 299 :: 300 :: Содержание




    Содержание  Назад  Вперед