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

82 2) запись дизъюнкции  [ С 1 ] и  [ C 2 ] без изменения порядка их литер:  [ С 1 ] V  [ C 2 ] ; 3) заключение  [ L 1 ] в рамку; 4) удаление  [ L 2 ] ; 5) вычеркиваем из выражения необрамленную литеру, кото- рая идентична младшей, не обрамленной литере; 6) вычеркиваем обрамленную литеру, идентичную младшей обрамленной литере; 7) применение операции сокращения. OL-вывод. Линейный вывод дизъюнкта С n из S с начальным дизъюнктом C 1 называется OL -выводом, если выполнены следую- щие условия: 1) для i = 1, 2, ..., n – 1, C i+ 1 является упорядоченной резоль- вентой дизъюнкта C i (центральный упорядоченный дизъюнкт) и B i (боковой упорядоченный дизъюнкт). При этом резольвируемая ли- тера в С i (или в упорядоченном факторе C i ) является последней ли- терой C i ; 2) B i является или некоторым дизъюнктом C j ( j < i ) (если C j – приведенный упорядоченный дизъюнкт), или дизъюнктом из S . Если B i – есть некоторый дизъюнкт C j ( j < i ) , то C i – приведенный упорядоченный дизъюнкт; 3) в выводе нет тавтологий. Рассмотрим пример доказательства методом линейной резо- люции. Пусть необходимо доказать, что «Каждый художник любит природу», и даны следующие правила: 1. «Не существует такого художника, который не пишет кар- тины». 2. «Каждый человек, пишущий картины, посещает художест- венный музей». 3. «Неправда, что существует человек, посещающий художе- ственный музей и не восхищающийся картинами Шишкина».