Библиотека >> К онтологии сознания через рефлексию
Скачать 164.78 Кбайт К онтологии сознания через рефлексию
Третий параграф ("Логико-эвристические исчисления) посвящен анализу использования в логических исчислениях идеи глобальной обработки информации и метода метапеременных, реализация которых привела к построению собственно интеллектуальных логических систем — логико-эвристических исчислений. В первой части параграфа ("Идея глобальной обработки информации в ТПВ") проводится исследование использования идеи глобальной обработки информации в ТПВ. Для этого выделяются два возможных направления реализации идеи глобальной обработки информации. Одно из них связано с дальнейшим анализом структуры вывода, что уже было намечено в рамках логических исчислений типа систем натурального вывода и секвенциальных исчислений. Например, при "глобальной" обработке секвенциального дерева вывода возможно извлечение информации о "расщеплении" некоторой формулы, что позволяет не производить "расщепление" такой же формулы в других ветвях дерева поиска. Во-вторых, возможно и более радикальное использование идеи глобальной обработки информации в виде построения специальных логических исчислений, более полно учитывающих информацию (структуру) испытуемых на выводимость формул, — исчислений поиска вывода. Далее анализируются конкретные системы поиска вывода, в которых идея глобальной обработки информации нашла свою реализацию. Это в основном работы, выполненные в ленинградской (петербургской) школе математической логики Н.А. Шанина: Н. Шанин и др. [9], Г. Давыдов [10], Г. Цейтин [11], П. Суворов [12], Е. Данцин [13]. В связи с анализом подхода Г.С. Цейтина, обсуждается еще один способ повышения эвристичности исчислений — использование собственно допустимых правил вывода (правил типа сечения). Анализ результатов теории сложности о существенном повышении "мощности" исчислений при использовании собственно допустимых правил вывода и установление связи между понятиями "собственно допустимое правило вывода" и "аналитического" ("не-аналитического") применения правила вывода позволяет сформулировать и обосновать тезис о существенном повышении эффективности систем поиска при использовании не-аналитических правил вывода. Далее отмечается, что самой значительной попыткой реализации идеи глобальной обработки информации в 60-е годы можно считать появление обратного метода С.Ю. Маслова, который синтезировал оба выделенных выше подхода использования идеи глобальной обработки информации. Анализ особенностей секвенциальных исчислений, используемых для организации поиска вывода, позволил выделить "генетические" идеи, которые лежат в основе создания ОМ и проясняют "суть" его работы, среди которых наиболее существенными являются идеи переворачивания направления поиска и использование структурной информации о "зацепленности" литер формулы. В заключении этой части параграфа кратко обсуждаются возможности использования идеи глобальной обработки информации в других типах логических исчислений и выделяется еще один интересный подход повышения эвристичности логических систем, который связан с использованием тернарных логических связок для структурного представления выводов и организации поиска вывода в исчислении высказываний . Во второй части параграфа ("Метод метапеременных в ТПВ") дается краткое концептуальное изложение идеи метода метапеременных. Определяется конкретизация этого метода для теории поиска вывода (логики) — метод временных переменных. Выделяется основная идея этого метода — "откладывание в долгий ящик" окончательного подбора значений термов при подстановке до тех пор, пока не будет получена недостающая информация о значении этих термов. Примерами использования этой идеи служат, например, понятие наиболее общего унификатора в методе резолюций Дж. Робинсона и понятие связки в обратном методе С. Маслова. В заключении главы отмечается, что представляется перспективным для теоретического анализа ТПВ использовать математический аппарат дедуктивной информации исчислений, основы которого были разработаны С.Ю. Масловым. Обобщение результатов, полученных при анализе истории развития ТПВ позволяет выделить наиболее интересные направления ее дальнейшего развития. Во второй главе ("Обратный метод С.Ю. Маслова") ставится задача построения на базе обратного метода С.Ю. Маслова [14] исчисления поиска вывода — исчисления чисел с индексами с целью моделирования на его основе разных тактик поиска вывода. Первый параграф ("Общая схема обратного метода") посвящен построению некоторой конкретизации обратного метода для исчисления высказываний. Пусть нам дана формула F в дизъюнктивной нормальной форме: a Ъ ~a&b Ъ a&~b Ъ ~a&~b и секвенциальное исчисление G без структурных правил и с допустимым правилом сечения: АКСИОМАМИ данного исчисления являются секвенции вида ® A, X, ~X, B, которые содержат контрарную пару литер. Страницы:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
| ||
|