Мивар: Линейный логический вывод. Олег Варламов
Чтение книги онлайн.
Читать онлайн книгу Мивар: Линейный логический вывод - Олег Варламов страница 3
В общем виде продукции встречаются весьма редко. Отметим, что существует аналогичный подход, основанный на гиперправилах с мультиактивизаторами [4]. Хорошевский В.Ф. в [31, стр. 82-83] при описании "слоеного пирога"SemanticWeb выделяет промежуточный "слой правил", для которого ведутся исследования различных систем вывода на правилах.
Под логической обработкой принято понимать некий вывод, лежащий в основе человеческих рассуждений. Для проведения анализа используем описания и исходную информацию из широко известных источников. В работе Поспелова Д.А. выдвинуто следующее основополагающее положение: "Всякий вывод, как бы он не был организован, носит переборный характер. … программа вынуждена перебирать варианты, заходить в тупики, проходить циклы прежде, чем она сможет найти правильный путь решения. Повышение эффективности процесса вывода – центральная проблема всех автоматизированных систем дедуктивного вывода" [23, стр. 79].
Особый интерес представляет описание общей схемы выводов, лежащей "в основе большого количества моделей человеческих достоверных рассуждений" [23, стр. 83]. Сначала Поспелов Д.А. приводит такое описание в виде некоторого дерева вывода: "Вершинам этого дерева соответствуют определенные утверждения Fi, а дуги определяют порядок получения новых утверждений. Те дуги, которые сходятся в зачерненные точки, образуют конъюктивные условия вывода, а те дуги, которые между собой соединены "дужкой", образуют дизъюнктивные условия вывода. … Дерево вывода с такими условиями переходов от вершины к вершине носит название И-ИЛИ дерева. В И-ИЛИ дереве ориентация дуг показывает направление вывода. Естественное разбиение вершин дерева по ярусам отражает глубину вывода (число шагов, необходимых для получения утверждений данного яруса). Первый ярус дерева образуют вершины… играющие роль аксиом или утверждений, истинность которых задается извне" [23, стр. 83-84]. Однако далее Поспелов Д.А. пишет: "Схема вывода не обязательно описывается в виде дерева. Она может иметь вид произвольной сети, ориентированной, неориентированной или частично ориентированной" [23, стр. 84]. На рисунке 1 показан пример неориентированной сети, аналогичный рисунку в [23, стр. 83]. "Такая сеть (наличие или отсутствие ориентации не играет здесь роли) называется И-ИЛИ сетью. Процесс вывода на И-ИЛИ сети протекает следующим образом. Пусть мы хотим доказать утверждение F6 (на рисунке 1 этому соответствует целевая вершина (выделена двойным контуром)). В качестве априорно доказанного задано утверждение F1 (ему соответствует начальная вершина, которая на рисунке 1 заштрихована). Как из F1