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

Пакко заклейщики коробов.          

Логические системы


В основе логических систем представления знаний лежит понятие формальной логической системы. Оно является также одним из основополагающих понятий формализации. Основные идеи формализации заключаются в следующем. Вводится множество базовых элементов (алфавит) теории. Определяются правила построения правильных объектов (предложений) из базовых элементов. Часть объектов объявляется изначально заданными и правильными по определению - аксиомами. Задаются правила построения новых объектов из других правильных объектов системы (правила вывода).

Данная схема лежит в основе построения многих дедуктивных СИИ. В соответствии с ней база знаний описывается в виде предложений и аксиом теории, а механизм вывода реализует правила построения новых предложений из имеющихся в базе знаний. На вход СИИ поступает описание задачи на языке этой теории в виде запроса (предложения, теоремы), которое явно не представлено в БЗ, но если оно верно с позиций заложенных в БЗ знаний и не противоречит им, то может быть построено из объектов БЗ путем применения правил вывода. Процесс работы механизма вывода называют доказательством запроса (теоремы). Если запомнить шаги процесса вывода в виде трассы и представить ее пользователю, то она будет объяснением выработанного СИИ решения задачи.

Формальные языки, на которых записываются предложения (формулы) с использованием рассмотренных понятий, получили названия логических языков. С практической и теоретической точек зрения наиболее важными и изученными являются язык логики высказываний и язык логики предикатов. В языке логики высказываний элементарные предложения рассматриваются как неделимые сущности, в языке логики предикатов, наоборот, делается расчленение предложения на субъект и предикат.

В процессе математизации рассуждений различают два вида слов: термы - аналоги имен существительных и формулы - аналоги повествовательных предложений.

Для записи предложений используются стандартные формы высказываний, что даёт возможность, с одной стороны, стандартизовать рассуждения, т.е.
рассматривать только определённые структуры посылок и заключений, а с другой - ввести в термы переменные - именные формы, которые обращаются в имена после подстановки вместо переменных конкретных значений.

Формулы с переменными, обращающиеся в высказывания при подстановке вместо переменных значений, называют высказывателъными формами или переменными высказываниями. Одна форма порождает множество истинных или ложных высказываний.

Однако не все предложения, содержащие переменные, являются высказывательными формами. Различают связанные и свободные переменные. Так, сложные предложения с переменными, содержащие логические связки СУЩЕСТВУЕТ или ВСЕ, обозначают высказывания, а переменные, к которым они относятся, являются связанными.

297

Расчленение предложения на субъект и предикат в математической логике математизируется путем соотнесения предложения, выражающего свойства предмета, с функцией одной переменной Р(х). При этом сама функция Р - логическая функция одной переменной, т. с. одноместный предикат, а аргумент х - субъект. Если же предложение описывает отношение между несколькими (п) субъектами, то с ним можно связать n-местную логическую функцию Р(х1 ,х2...хп) - n-местный предикат.

Логические связки "И", "ИЛИ", "НЕ" и т.д., с помощью которых строятся сложные предложения (формулы), соотносятся с операциями логики следующим образом:



НЕВЕРНО ЧТО - ¬ (знак отрицания);
И - ? (знак конъюнкции);
ИЛИ - ? (знак дизъюнкции);
ЕСЛИ ... ТО - > (знак импликации);
ТОГДА, КОГДА - ? (знак эквивалентности).
Логические связки "ДЛЯ ВСЯКОГО", "СУЩЕСТВУЕТ" относятся к переменным в предложении и обозначают:

ДЛЯ ВСЯКОГО - ? (знак квантора общности);
СУЩЕСТВУЕТ - ? (знак квантора существования).
В различных логических системах используются разнообразные правила вывода. Приведем два наиболее распространенных из них.

Первое - "правило подстановки" имеет следующую формулировку. В формулу, которая уже выведена, можно вместо некоторого высказывания подставить любое другое при соблюдении условия: подстановка должна быть сделана во всех местах вхождения заменяемого высказывания в данную формулу.



Второе - "правило заключения" (латинское название Modus Ponens - положительный модус) состоит в следующем: Если а и ? > ? являются истинными высказываниями посылками, тогда и высказывание заключение ? также истина. Записывается правило в виде дроби:

α, α → β
β
Пример. Пусть имеются следующие истинные высказывания:

  • Если самолет проверен и заправлен, то он готов к вылету.


  • Если самолет готов к вылету и дано разрешение на взлет, то он либо взлетел, либо находится па взлётной полосе.


  • Если самолет взлетел, то он выполняет рейс.


  • Самолет ЯК-42 проверен и заправлен.


  • Самолет ТУ-134 проверен.


  • Самолет ИЛ-62 заправлен.


  • Самолету ЯК-42 дано разрешение на вылет.


  • Самолет ЯК-42 не находится на взлетной полосе.


  • Требуется найти, какой из самолетов в момент времени Т выполняет рейс.

    Проведем анализ данных высказываний. Высказывания 1, 2, 3 являются сложными и построены с использованием логических связок > (импликация), ? (И). Во всех элементарных высказываниях, из которых построены предложения 1,2,3, субъектом является

    298

    понятие "самолет"; предикатами выступают сказуемые, описывающие свойства всех объектов, принадлежащих классу "самолет". Высказывания 4-8 являются фактами, истинными на момент времени Т. Они являются элементарными высказываниями, описывающими свойства конкретных объектов предметной области.

    Для формального описания задачи введем следующие одноместные предикаты:

    ПРОВЕРЕН(Х) - самолет X проверен;

    ЗАПРАВЛЕН(Х) - самолет X заправлен;

    ГОТОВ(Х) - самолет X готов к вылету;

    ДАНО_РАЗР(Х) - самолету X дано разрешение на вылет;

    ВЗЛЕТЕЛ(Х) - самолет X взлетел;

    НАХ_ВЗП(Х) - самолет X находится на взлетной полосе;

    НЕ_НАХ_ВЗП(Х) - самолет X не находится на взлетной полосе;

    ВЫП_РЕЙС(Х) - самолет X выполняет рейс.

    Тогда исходное описание на языке логики предикатов будет иметь вид:

  • ?Х(ПРОВЕРЕН(Х)? ЗАПРАВЛЕН(Х) > ГОТОВ(Х))


  • ?Х(ГОТОВ(Х) ? ДАНО_РАЗР(Х)иНЕ_НАХ_ВЗП(Х) > ВЗЛЕТЕЛ(Х))


  • ?Х(ГОТОВ(Х) ? ДАНО_РАЗР(Х)1Ю ВЗЛЕТЕЛ(Х) > НАХ_ВЗП(Х))




  • ?Х(ВЗЛЕТЕЛ(Х) > ВЫП_РЕЙС(Х))


  • ПРОВЕРЕН(ЯК-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 :: Содержание


    Содержание раздела