Напишем:


✔ Реферат от 200 руб.
✔ Контрольную от 200 руб.
✔ Курсовую от 500 руб.
✔ Решим задачу от 20 руб.
✔ Дипломную работу от 3000 руб.
✔ Другие виды работ по договоренности.

Узнать стоимость!

Не интересно!

 

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

  • Увеличить размер шрифта
  • Размер шрифта по умолчанию
  • Уменьшить размер шрифта

Принцип резолюции

 Если матрица формулы в результате приведения к виду ПНФ не будет содержать свободных переменных и сколемовских функций, то для вывода заключения полностью пpuменим алгоритм принципа резолюции, рассмотренный в исчислении высказываний. Этот алгоритм основывается на том, что если две формулы состоящие из дизъюнкции атомов (в дальнейшем такие формулы будем называть дизъюнктами ) связаны конъюнкцией, и в них имеются два одинаковых или приводимых к одинаковым (унифицируемых ) атома с разными знаками, то из них можно получить третий дизъюнкт , который будет логическим следствием первых двух, и в нем будут исключены эти два атома. Однако, если в результате приведения к виду ССФ аргументы атомов содержат сколемовские функции, то для поиска контрарных атомов необходимо выполнить подстановки термов вместо предметных переменных и получить новые формулы дизъюнктов, которые допускают их унификацию при формировании контрарных пар. Множество подстановок нужно формировать последовательно, просматривая каждый раз только одну предметную переменную.

Например, если даны два дизъюнкта (P1(x)ÚùP2(x)) и (ùP1(f(x))ÚP3(y)), то для получения контрарной пары атомов возможна подстановка

      xòf(х)(P1(x)ÚùP2(x))=(P1(f(x))ÚùP2(f(x))) и

xòf(х)(ùP1(f(x))ÚP3(y))= (ùP1(f(x))ÚP3(y)).

В результате склеивания этих дизъюнктов может быть получена резольвента: (P1(f(x))ÚùP2(f(x)))Ú(ùP1(f(x))ÚP3(y))= (ùP2(f(x))Ú P3(y)).

Если пара дизъюнктов имеет вид (P1(f1(x))ÚùP2(x)) и (ùP1(f2(x))ÚP3(y)), то никакая подстановка не позволит сформировать резольвенту.

 

Пример: Даны  две формулы P3(a;x;f(q(y))) и ùP3(z;f(z);f(u)).

Выполнить унификацию контрарных атомов.

1) zòa ùP3(z;f(z);f(u))=ùP3(a;f(a);f(u));

2) xòf(a) P3(a;x;f(q(y)))=P3(a;f(a);f(q(y)));

3) uòq(y) ùP3(a;f(a);f(u))=ùP3(a;f(a);f(q(y))).      

В результате получены два контрарных атома: P3(a;f(a);f(q(y))) и ùP3(a;f(a);f(q(y))). Если в эти формулы атомов вместо предметной переменной y сделать подстановку предметной постоянной b, т.е.

yòbP3(a;f(a);f(q(y)))=P3(a;f(a);f(q(b))) и

yòbùP3(a;f(a);f(q(y)))= P3(a;f(a);f(q(b))),

то получим два контрарных высказывания.

Пример. Даны две формулы P3(x;a;f(q(a))) и ùP3(z;y;f(u)).

Выполнить унификацию контрарных формул.

1) xòbP3(x;a;f(q(a)))=P3(b;a;f(q(a)));

2) yòaù P3(z;y;f(u))=ùP3(z;a;f(u));

3) yòaùP3(z;a;f(u))=ùP3(b;a;f(u));

4) uòq(a)ùP3(b;a;f(u))=ùP3(b;a;f(q(a))).

В результате получены две контрарных формулы: P3(b;a;f(q(a))) и ùP3(b;a;f(q(a))).

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

Линейным выводом из множества дизъюнктов K называется последовательность дизъюнктов D1, D2,...Dn, где каждый член DiÎK, а каждый Di+1 является резольвентой центрального дизъюнкта (или предшествующей резольвенты) и бокового дизъюнкта из множества K.

Упорядоченным дизъюнктом называется дизъюнкт с заданной последовательностью атомов. Атом Pj старше атома Pi в упорядоченном дизъюнкте тогда и только тогда, когда  j > i. Например, в упорядоченном дизъюнкте (P1ÚP2ÚP3ÚP4) младшим считается атом P1, а старшим - P4. При наличии в упорядоченном дизюънкте двух одинаковых атомов, по закону идемпотенции, следует удалить старший атом, сохранив на прежнем месте младший.

Другим усилением принципа резолюции является использование информации о резольвируемых атомах. Обычно при выполнении процедуры унификации происходит удаление резольвируемых атомов. Од­нако они несут полезную информацию. Поэтому вмес­то удаления резольвируемых атомов при унификации предлагается удалять только старший атом, а младший - сохранить в резольвенте, выделив какой-либо рамкой. Если за обрамленным атомом в резольвенте не следует никакой другой атом, то обрамленный атом удалить. Если за обрамленным атомом резольвенты следует какой-либо необрамленный атом, то его следует оставить для последующего исследования. И наконец, если последний необрамленный атом резольвенты унифицируется с отрицанием атома боковой ветви, то его следует обрамить и удалить вместе с литерой боковой ветви. Используя резольвенты на последующих этапах, можно получить обрамленными все атомы последней резольвенты, т.е.получить пустой дизъюнкт.

Пример: Суждение “Преподаватели принимали зачеты у всех студентов, не являющихся отличниками. Некоторые аспиранты и студенты сдавали зачеты только аспирантам. Ни один из аспирантов не был отличником. Следавательно, некоторые преподаватели были аспирантами.” [1] Пусть P1(x):=”x – отличник”, P2(x):=”x – аспирант”, P3(x):=”x –студент”, P24 (x; y):=”x сдает зачет y”, P5(x):=”x – преподаватель”. Формулы  этого суждение имеют вид:


 

"x(P3(x)&ùP1 (x)®$y(P5(y)&P24 (x; y))); $x(P2(x)&P3(x)&"y(P24 (x; y)®P2 (y)));

"x(P2(x)®ùP1(x)) .

Принцип резолюции$x(P5(x)&P2(x)).

·        Преобразовать посылки и отрицание заключения в ССФ:

1) F1="x(P3(x)&ùP1 (x)®$y(P5(y)&P24 (x; y)))=

"x$y(P3(x)&ùP1 (x)®(P5(y)&P24 (x; y)))=

"x(P3(x)&ùP1 (x)®(P5(f(x))&P24 (x; f(x)))).

        M1=(P3(x)&ùP1 (x)®P5(f(x))&P24 (x; f(x)))=

ù(P3(x)&ùP1 (x))Ú P5(f(x))&P24 (x; f(x)) =

(ùP3(x)ÚP1 (x)Ú P5 (f(x))&P24 (x; f(x))=

(ùP3(x)ÚP1 (x)Ú P5(f(x)))&(ùP3(x)ÚP1 (x)Ú P24 (x; f(x))).

2) F2=$x(P2(x)&P3(x)&"y(P24 (x; y)®P2 (y)))=

$x"y(P2(x)&P3(x)&(P24 (x; y)®P2 (y)))=

"y(P2(a)&P3(a)&(P24 (a; y)®P2 (y))).

    M2=(P2(a)&P3(a)&(P24 (a; y)®P2 (y)))=

P2(a)&P3(a)&(ùP24 (a; y)ÚP2 (y))).

3) F3="x(P2(x)®ùP1(x)).

M3=(P2(x)®ùP1(x))= (ùP2(x)ÚùP1(x)).

4) F4=ù$x(P5(x)&P2(x))= "x(ù (P5(x)&P2(x))).

M4=(ù (P5(x)&P2(x)))= (ùP5(x)Úù P2(x))).

·        Выписать множество дизъюнктов:

K= {(ùP3(x)ÚP1 (x)ÚP5(f(x))); (ùP3(x)ÚP1 (x)Ú P24 (x; f(x))); P2(a); P3(a);
(ùP24 (a; y)ÚP2(y)); (ùP1(x)ÚùP2(x)); (ùP5(x)ÚùP2(x))};

 

·        Выполнить унификацию и формирование резольвент

ùP2(a)

 
1) xòa (ùP1(x)ÚùP2(x)) Ú P2(a)= ùP1(a)Ú          = ùP1(a);

ùP1(a)

 
2)ùP1(a)Úxòa(ùP3(x)ÚP1 (x)ÚP24 (x; f(x)))=                ÚùP3(a)Ú P24 (a; f(a));

ùP1(a)         1(a)

 
3)                 ÚùP3(a) Ú P24 (a; f(a))Ú yòf(a) (ùP24 (a; y)ÚP2(y))=

P24 (a; f(a))

 

ùP1(a)

 
            ÚùP3(a)Ú                       Ú P2(f(a));

P24 (a; f(a))

 

ùP1(a)

 
4)                    ÚùP3(a)Ú                     Ú P2(f(a)) Úxòf(a)(ùP5(x)ÚùP2(x))=

P24 (a; f(a))

 

P2(f(a))

 

ùP1(a)

 
                       ÚùP3(a)Ú                    Ú                  ÚùP5(f(a));

P24 (a; f(a))

 

P2(f(a))

 

ùP1(a)

 
5)                   ÚùP3(a)Ú                     Ú                    ÚùP5(f(a)) Ú

P2(f(a))

 

ùP5(f(a))

 

P24 (a; f(a))

 

ùP1(a)

 
xòa(ùP3(x)ÚP1 (x)ÚP5(f(x)))=                ÚùP3(a)Ú                     Ú                Ú                        Ú P1 (a);

P24 (a; f(a))

 

ùP1(a)

 

P2(f(a))

 

ùP5(f(a))

 
6)                     ÚùP3(a)Ú                              Ú                  Ú                    Ú P1 (a)ÚùP1(a)=

ùP5(f(a))

 

P2(f(a))

 

P24 (a; f(a))

 

P1(a)

 

ùP1(a)

 
          ÚùP3(a)Ú                       Ú                  Ú                    Ú                =

ùP1(a)

 
ÚùP3(a);

ùP3(a)

 

ùP1(a)

 

ùP1(a)

 
    7)                     ÚùP3(a) Ú P3(a)=                             Ú                          = .        

 

На рис. 14 дан граф линейной унификации этого примера.        

 

Принцип резолюции                                         ùP1(x)ÚùP2(x)

Принцип резолюции                                                                      ùP1(a)          P2(a)

ùP1(a)

 
Принцип резолюции                                                ÚùP3(a)Ú P24 (a; f(a))           ùP3(x)ÚP1 (x)ÚP24 (x; f(x))

Принцип резолюции

ùP1(a)

 

P24 (a; f(a))

 
                            ÚùP3(a)Ú                   Ú P2(f(a))             ùP24 (a; y)ÚP2(y)

Принцип резолюции

ùP1(a)

 

P24 (a; f(a))

 

P2(f(a))

 
                        ÚùP3(a) Ú                     Ú              Ú         ùP5(x)ÚùP2(x)

ùP1(a)

 

P24 (a; f(a))

 

P2(f(a))

 
                                            ÚùP5(f(a))

Принцип резолюции            ÚùP3(a)Ú                        Ú               Ú          ùP3(x)ÚP1 (x)ÚP5(f(x))

ùP1(a)

 

ùP5(f(a))

 
                          Ú                      ÚP1 (x)

Принцип резолюции                                                         ÚùP3(a)          ùP1(a)

               Принцип резолюции    P3(a)

Рис. 14. Граф линейной унификации

 

      Пример: Существуют студенты, которые любят всех преподавателей. Ни один из студентов не любит невежд. Следовательно, ни один из преподавателей не является невеждой. [1]     

Пусть P1(x):=” x – студент”, P2(y):=”y – преподаватель”, P23(x, y):=”x любит y”, P4(y):=”y - невежда”.

Формулы этого суждение имеют вид:

$x(P1(x)&"y(P2 (y)®P23(x; y)));


Принцип резолюции"x(P1(x) ®"y(P4  (y)®ùP23(x; y)));

"y(P2  (y)®ùP4(y));

·        Преобразовать посылки и отрицание заключения в ССФ:

1)    F1=$x(P1(x)&"y(P2 (y)®P23(x; y)))= $x"y(P1(x)& (P2 (y)®P23(x; y)))= "y(P1(a)& (P2 (y)®P23(a; y)))= "y(P1(a)& (ùP2 (y)ÚP23(a; y)));

M1= P1(a)&(ùP2 (y)ÚP23(a; y));

2)    F2="x(P1(x) ®"y(P4  (y)®ùP23(x; y)))=

 "x"y (P1(x) ® (P4  (y)®ùP23(x; y)))= "x"y (ùP1(x)ÚùP4  (y)ÚùP23(x; y)));

M2=(ùP1(x)ÚùP4  (y)ÚùP23(x; y));

3)    F3=ù"y(P2  (y)®ùP4(y))= $y(ù(ùP2(y)ÚùP4(y))= $y(P2(y) &P4(y))=

 P2(b)&P4(b);

M3=P2(b)&P4(b).

·              Выписать множество дизъюнктов:

K={P1(a); (ùP2 (y)ÚP23(a; y)); (ùP1(x)ÚùP4  (y)ÚùP23(x; y)); P2(b); P4(b)};

·        Выполнить унификацию и формирование резольвент:

 

P2(b)

 
1) P2(b) Ú xòb(ùP2 (y)ÚP23(a; y))=            ÚP23(a; b);

P2(b)

 
    2)              ÚP23(a; b)Úyòb (ùP1(x)ÚùP4  (y)ÚùP23(x; y))=

P2(b)

 
                    ÚP23(a; b)Ú(ùP1(x)ÚùP4  (b)ÚùP23(x; b));

P2(b)

 
3)              ÚP23(a; b)Úxòa(ùP1(x)ÚùP4  (b)ÚùP23(x; b))=

Ú   

P23(a; b)

 

P2(b)

 
                ÚùP1(a)ÚùP4  (b);

P2(b)

 

P23(a; b)

 
4)               Ú                            ÚùP1(a)ÚùP4  (b) ÚP1(a)=

P2(b)

 

P23(a; b)

 

ùP1(a)

 
                        Ú                    Ú                 ÚùP4  (b);

ùP1(a)

 

P23(a; b)

 

P2(b)

 
5)               Ú                    Ú                ÚùP4  (b) ÚP4(b)=                      

ùP4 (b)

 

ùP1(a)

 

P23(a; b)

 

P2(b)

 
Ú                   Ú               Ú                = .

 

 На рис. 15 приведен граф линейной унификации для этого примера.

Принцип резолюцииP2(b)

P2(b)

 

P2(b)

 
Принцип резолюции          ÚP23(a; b)           ùP2 (y)ÚP23(a; y)

Принцип резолюции    ÚP23(a; b)Ú (ùP1(x)ÚùP4  (b)Ú           ùP1(x)ÚùP4  (y)ÚùP23(x; y)

P23(a; b)

 

P2(b)

 
                       ÚùP23(x; b))                            

ùP1(a)

 
Принцип резолюции                   Ú                  ÚùP1(a) ÚùP4  (b)            ùP1(x)ÚùP4  (b)ÚùP23(x; b))

Принцип резолюции

P23(a; b)

 

P2(b)

 
        Ú                  Ú              ÚùP4  (b)          P1(a)

Принцип резолюции                                                             P4(b)

      

Рис. 15. Граф линейной унификации