Представление и обработка знаний

81 P V R P V R V  P  P V  R P V R  P V R P V R P V  R P P Рис. 3.6. Пример линейного вывода с использованием обрамленной литеры Подчеркнутая резольвента. Если в резольвенте литера L яв- ляется отрицанием какой-либо обрамленной литеры, то резольвен- та подчеркивается. Если встречается подчеркнутая резольвента, то в качестве второго дизъюнкта контрарной пары используется цен- тральный дизъюнкт (см. * на рис. 3.6). Приведенный упорядоченный дизъюнкт. Упорядоченный дизъюнкт С будем называть приведенным упорядоченным дизъ- юнктом, если его последняя литера является подчеркнутой, т.е. унифицируется с отрицанием обрамленной литеры. После ре- дукции эта литера становится обрамленной. Если эта литера после редукции остается последней, то она вычеркивается. Эта операция называется операцией приведения (см. * на рис. 3.6). Приведенный упорядоченный дизъюнкт образуется при выполнении операций приведения и сокращения. Упорядоченная бинарная резольвента. Пусть С 1 и С 2 – упо- рядоченные дизъюнкты, которые содержат литеры L 1 и L 2 = ¬ L 1 со- ответственно, L 1 и L 2 могут быть унифицированы наиболее общим унификатором  . Тогда упорядоченная бинарная резольвента С – это упорядоченный дизъюнкт, полученный следующим образом: 1) выполнение подстановок и определение  [ С 1 ] и  [ C 2 ] ; Р (*)