Интеллектуальные информационные системы. Макаренко С.И. - 64 стр.

    Примером логического знания формализованного в виде логики
предикатов высших порядков является знание: «Когда температура в печи
достигает 1200 и прошло менее 30 мин с момента включения печи, давление
не может превосходить критическое. Если с момента включения печи
прошло более 30 мин, то необходимо открыть вентиль №2».
    Логическая модель представления этого знания имеет вид:
                      P(p = 120) T(t<30) → (D < Dкp);
                        Р(р = 120) T(t>30) → F(№2).
    В этой записи использованы следующие обозначения для предикатов:
    Р(р = 120) — предикат, становящийся истинным, когда температура
    достигает 120 градусов,
    T(t < 30) — предикат, остающийся истинным в течение 30 мин с начала
    процесса;
    T(t > 30) — предикат, становящийся истинным по истечении 30 мин с
    начала процесса;
    (D < Dкр) — утверждение о том, что давление ниже критического;
    F(№2) — команда открыть вентиль №2.
    Кроме того, в записях использованы типовые логические связки
конъюнкции (v), импликации (^) и логического следования (→).
   Первая строчка в записи представляет декларативные знания, а вторая
— процедурные.
    Решение задач в логике предикатов сводится к доказательству целевого
утверждения в виде формулы или предиката (теоремы), используя известные
утверждения (формулы) или аксиомы.
     В конце 60-х годов Робинсоном для доказательства теорем в логике
предикатов был предложен метод резолюции, основанный на доказательстве
«от противного». Целевое утверждение инвертируется, добавляется к
множеству аксиом и доказывается, что полученное таким образом множество
утверждений является несовместным (противоречивым). Для выполнения
доказательства методом резолюции необходимо провести определенные
преобразования над множеством утверждений, а именно, привести их к
совершенной конъюнктивной нормальной форме (СКНФ). СКНФ
представляет собой набор (конъюнкцию) дизъюнктов без кванторов.
Кванторы всеобщности подразумеваются, а кванторы существования
заменяются на перечисление формул (или предикатов) со всеми константами
из предметной области, для которых формула истинна. Например:
    «отец (Иван, Петр)», «отец (Иван, Степан)» и т.д.



                                    63