Главная    Ex Libris    Книги    Журналы    Статьи    Серии    Каталог    Wanted    Загрузка    ХудЛит    Справка    Поиск по индексам    Поиск    Форум   
blank
Авторизация

       
blank
Поиск по указателям

blank
blank
blank
Красота
blank
Чень Ч., Ли Р. — Математическая логика и автоматическое доказательство теорем
Чень Ч., Ли Р. — Математическая логика и автоматическое доказательство теорем



Обсудите книгу на научном форуме



Нашли опечатку?
Выделите ее мышкой и нажмите Ctrl+Enter

Название: Математическая логика и автоматическое доказательство теорем

Авторы: Чень Ч., Ли Р.

Аннотация:

Книга посвящена детальному изложению всего круга проблем, связанных с так называемым методом резолюций. Этот метод наиболее известен и широко используется в современных работах по доказательству на ЭВМ математических теорем и вообще при построении систем «искусственного интеллекта». Описываются применения метода к таким, например, актуальным для всякого системного программиста задачам, как автоматический анализ и синтез программ. В приложении описаны другие методы и некоторые результаты последних лет, знакомство с которыми необходимо при изучении
проблематики автоматического доказательства теорем.


Язык: ru

Рубрика: Математика/Алгебра/Математическая логика/

Статус предметного указателя: Готов указатель с номерами страниц

ed2k: ed2k stats

Год издания: 1983

Количество страниц: 360

Добавлена в каталог: 10.05.2005

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID
blank
Предметный указатель
$\alpha$-дизъюнкт      320
$\alpha$-истинная литера      320
$\Pi$-стратегия      329
$\Pi$-стратегия слабая      329
$\Sigma$-набор      302
c-правило      295
E-интерпретация (E-interpretation)      162
f-атом      308
f-набор      301
f-подстановка      304
H-интерпретация (H-interpretation)      60; (см. также «Интерпретация»)
n-местный предикатный символ (n-place predicate symbol)      36
n-местный функциональный символ (n-place function symbol)      36
OI-вывод (OI-deduction)      117
OI-клаш (OI-clash)      115
OI-резольвента (OI-resolvent)      116
OL-вывод (OL-deduction)      139
OL-опровержение (OL-refutation)      139
P-гиперпарамодулянт (P-hyperparamodulant)      166
PI-вывод (PI-deduction)      107
PI-клаш (PI-clash)      105
PI-резольвента (PI-resolvent)      106
r-литерный дизъюнкт (r-literal clause)      55
S-входной вывод (S-input deduction)      132
V-гиперрезолюция (V-hyperresolutionj      186
V-парамодулянт (V-paramodulant)      190
V-парамодуляция (V-paramodulation)      190
V-резольвента (V-resolvent)      185
V-резолюция (V-resolution)      184
V-резолюция с множеством поддержки (set-of-support V-resolution)      186
V-склейка (V-factor)      185
А-правило      01 302 304
Абрахамс      72 282 288
Августин      69
Аккерман      2 49 268 270
Аксиома (axiom)      6
Аксиома индукции (induction axiom)      58—261
Аксиома равенства (equality axiom)      63
Аксиома рефлексивности (functionally reflexive axiom)      162
Алгорифм Британского музея      314
Алгорифм извлечения информации (information-extraction algorithm)      237
Алгорифм поглощения (subsumption algorithm)      98
Алгорифм синтеза программ (program-synthesizing algorithm)      250 261
Алгорифм унификации (unification algorithm)      82
Амарел      269
Анализ программ с помощью резолюции (program analysis by resolution)      211—215
Андерсон      10 53 72 102 118 125 126 130 156 166 176
Ассоциативный закон (associative law)      22
Атом (atom)      см. также «Атомарная формула»
Атом в логике высказываний (atom in propositional logic)      16
Атом в логике первого порядка (atom in first-order logic)      37
Атом основной (ground atom)      59
Атомарная формула (atomic formula)      16 38
Ацикличный порядок      339
Б-правило      301 302 304
Базис эрбрановский (Herbrand base)      60
Басекер      207 224
Берстол      261 264
Бинарная лок-резольвента (binary lock resolvent)      123
Бинарная резольвента (binary resolvent)      85; (см. также «Резольвента»)
Бинарный парамодулянт (binary paramodulant)      165
Бледсоу      53 72 102 125 126 130 156 199 201 268 269
Блек      227 264
Бойер      53 72 102 122 126 127
Боковой дизъюнкт (side clause)      130
Боковой дизъюнкт упорядоченный (side ordered clause)      139
Боковой узел (side node)      172
Более ограничительная подстановка (more restrictive substitution)      198
Брайс      268 269
Бранд      169
Буль      12
Ван      72
Вариант (variant)      180
Вейсман      272 282 288
Верхний дизъюнкт (top clause)      130
Верхний узел (top node)      145
Ветвь (branch)      172
Вогера      73
Вопрос, допускающий ответ (answerable question)      241
Вригт      269 270
Вулф      227 264
Входная парамодуляция (input paramodulation)      169
Входная резолюция (input resolution)      132
Входное опровержение (input refutation)      132
Входной дизъюнкт (input clause)      132
Вывод (deduction)      78 292
Вывод S-входной (S-input deduction)      132
Вывод входной (input deduction)      132
Вывод единичный (unit deduction)      132
Вывод линейный (linear deduction)      130
Вывод примитивный (primitive deduction)      248
Вывод с поддержкой (set-of-support deduction)      111 219
Выводящий узел (inference node)      65
Выполнимая формула (satisfiable formula)      21 42
Выполнимость в логике высказываний (satisfability in propositional logic)      21
Выполнимость в логике первого порядка (satisfability in first-order logic)      42
Выражение основное (ground expression)      59
Высказывание (proposition)      16
Высказывание составное (compound proposition)      16
Высота решения      318
Высота системы уравнений в термах      318
Высота терма      317
Галил      72
Гелернтер      268 270
Генкин      268 270
Генцен      7 11 292 313
Гилмор      9 52 53 68 69 72
Гильберт      9 32 49 52 268 270
Гиперпарамодуляция (hyperparamodulation)      166
Гиперпарамодуляция, полнота (completeness of hyperparamodulation)      167
Гиперрезолюция (hyperresolution)      109
Гиперрезолюция отрицательная (negative hyperresolution)      110
Гиперрезолюция положительная (positive hyperresolution)      109
Глубина терма      308
Граница глубины (depth bound)      147
Граф ориентированный (directed graph)      207
Граф-схема (flowchart)      205
Грин, Б.      227 264
Грин, К.      227 231 233 234 242 264
Гулд      268 270
Давыдов, Г.В.      99 302 313
Данцин, Е.Я.      72
Дарлингтон      160 176 227 265 268 270
Девис      9 53 54 69 72 75 179 184 201 202 268 270
Дегтярев, А.И.      169
Дедуктивный поиск ответов на вопросы (deductive question answering)      227—242
Дерево вывода (deduction tree)      79 87 294;
Дерево поиска вывода      294
Дерксен      268 269
Дизъюнкт (clause)      55
Дизъюнкт r-литерный (r-literal clause)      55
Дизъюнкт боковой (side clause)      130
Дизъюнкт верхний (top clause)      130
Дизъюнкт входной (input clause)      132
Дизъюнкт единичный (unit clause)      55
Дизъюнкт жизненный (vital clause)      248
Дизъюнкт описывающий (describing clause)      210
Дизъюнкт основной (ground clause)      59
Дизъюнкт отрицательный (negative clause)      109
Дизъюнкт положительный (positive clause)      109
Дизъюнкт пустой (empty clause)      55
Дизъюнкт смешанный (mixed claused)      109
Дизъюнкт упорядоченный (ordered clause)      113
Дизъюнкт упорядоченный боковой (side ordered clause)      139
Дизъюнкт упорядоченный неотрицательный (nonnegative ordered clause)      118
Дизъюнкт упорядоченный неположительный (nonpositive ordered clause)      118
Дизъюнкт упорядоченный отрицательный (negative ordered clause)      118
Дизъюнкт упорядоченный положительный (positive ordered clause)      118
Дизъюнкт упорядоченный центральный (center order clause)      139
Дизъюнкт упорядоченныйредуцируемый (reducible ordered clause)      137
Дизъюнкт центральный (center clause)      130
Дизъюнкт-ответ (answering clause)      231
Дизъюнкт-посылка (parent clause)      85
Дизъюнктивная нормальная форма (disjunctive normal form)      23
Дизъюнкция (disjunction)      17 23
Диксон      162 176 222 224
Дистрибутивные законы (distributive laws)      22
Доказательство (proof)      13 78
Драгалин, А.Г.      317 325
Дрейпер      156
Единичная парамодуляция (unit paramodulation)      169
Единичная резолюция (unit resolution)      132
Единичная склейка (unit factor)      85
Единичное опровержение (unit refutation)      132
Единичный вывод (unit deduction)      132
Единичный дизъюнкт (unit clause)      55
Ейтс      53 72 130 156
Жизненная переменная (vital variable)      248
Жизненный дизъюнкт (vital clause)      248
Задача изоморфизма графов (graph isomorphism problem)      188—190
Задача о завершении работы (terminating problem)      204 215—218
Задача о правильности (correctness problem)      204 220—221
Задача о реакции (response problem)      204 215—218
Задача о специализации (specialization problem)      204 222—224
Задача об обезьяне и банане (monkey-banana problem)      234—235
Задача об эквивалентности (equivalence problem)      204 220—221
Заключение теоремы (conclusion of theorem)      26
Законы ассоциативные (associative laws)      22
Законы де Моргана (De Morgan's laws)      22
Законы дистрибутивные (distributive laws)      22
Законы коммутативные (commutative laws)      22
Закрытое псевдосемантическое дерево (closed pseudosemantic tree)      192
Закрытое семантическое дерево (closed semantic tree)      65
Зиберт      161 176
Значение истинностное (truth value)      16
Избыток литер (excess literal parameter)      125
Индивидный символ (individual symbol)      36 см. также Константа
Интерпретация в логике высказываний (interpretation in propositional logic)      18
Интерпретация первого порядка (interpretation in first-order logic)      39
Интерпретация частичная (partial interpretation)      65
Иохельсон      10
Истина при интерпретации (truth under an interpretation)      18 39
Истинностная таблица (truth table)      19
Истинностное значение (truth value)      16
Исчисление      292
Исчисление благоприятных наборов      301 302
Исчисление для нахождения первообразных      292
Исчисление задач на построение      295
Йенсен      268 270
Кальмар      315 324
Кангер      296—298 313
Карсон      53 73 102 111 127 133 156 176 199 202
Квантор всеобщности (universal quantifier)      37
Квантор существования (existential quantifier)      37
Квантор, область действия      (scope of quantifier)
Клаш семантический (semantic clash)      105
Клаш семантический упорядоченный (ordered semantic clash)      115
Клини      32 49 67 295 313 322 325
Кнут      67 72
Ковальский      53 63 72 98 100 102 127 128 130 135 138 156 166 176 268 270 326 332
Комбинация подстановок (combination of substitutions)      182
Коммутативные законы (commutative laws)      22
Композиция подстановок (composition of substitutions)      81
Конечный узел (terminal vertex)      207
Конивер      10 199 202
Константа (constant)      36
Контрарная пара (complementary pair)      64
Контрольная формула (testing formula)      208
Контрольный предикат (testing predicate)      208
Конъюнктивная нормальная форма (conjunctive normal form)      23
Конъюнкция (conjunction)      17 23
Копия (copy)      180
Корфаг      49
Крайзель      242 291 295 313
Крипке      269 270
Крисси      10
Куам      272 282 288
Куинлен      171 176
Курьеров, Ю.Н.      72 330 332
Кюнер      53 72 102 127 130 135 138 156 268 270
Лавленд      53 73 102 127 130 135 138 156 179 184 201
Лайтстоун      14 15
Лакхем      53 73 102 127 130 156
Левин      272 282 288
Лейбниц      9 52
Лемма Кёнига (Konig's lemma)      67
Лемма подъема (lifting lemma)      89
Ленгфорд      269 270
Ли      7 205 222 224 227 234 242 265 266
Линдсей      228 265
Линейная парамодуляция (linear paramodulation)      174—175
Линейная парамодуляция, полнота (completeness of linear paramodulation)      175
Линейная резолюция (linear resolution)      130
Линейная резолюция, полнота (completeness of linear resolution)      141—143
Линейный вывод (linear deduction)      130
ЛИСП (LISP)      205 269
Литера (literal)      23
Литера основная (ground literal)      59
Литера отрезаемая (literal resolved upon)      85
Литера парамодуляции (paramodulation upon literal)      65
Логика высказываний (propositional logic)      16—32
Логика высшего порядка (higher-order logic)      268
Логика модальная (modal logic)      268—269
Логика первого порядка (first-order logic)      35—49
Логические связки (logical connectives)      16
Логическое следствие в логике высказываний (logical consequence in propositional logic)      25
Логическое следствие в логике первого порядка (logical consequence in first-order logic)      43
Ложь (false)      16
Ложь при интерпретации (false under an interpretation)      18 29
Лок-вывод (lock deduction)      124
Лок-резольвента (lock resolvent)      123
Лок-резольвента бинарная (binary lock resolvent)      123
Лок-резолюция (lock resolution)      122
Лок-резолюция, полнота (completeness of lock resolution)      125—126
Лок-склейка (lock factor)      123
Лок-стратегия      329
Лофери      227 264
Луккези      268 270
Льюис      269 270
Макилрой      179 184 202
Маккарти      205 224 227 234 265 268 270 272 282 288
Манна      10 204 224 242 261 265
Маринов      268 271
Маслов, С.Ю.      72 99 291 296—299 302—304 308 313 326—328 331 332
Матрица (matrix)      44
Мельцер      53 73 102 127 159 176
Мендельсон      14 32 49 322 326
Метапеременная      297
Метод Девиса и Патнема (method of Davis and Putnam)      69
Метод Девиса и Патнема обобщенный (generalized method of Davis and Putnam)      200
Метод Девиса насыщения уровней (level-saturation method)      96
Метод поиска в глубину (depth-first method)      147
Метод поиска в глубину модифицированный (modified depth-first method)      149
Метод поиска в ширину (breadth-first method)      145
Метод резолюций (resolution principle)      77 85
Метод умножения (multiplication method)      31
Методы поиска вывода глобальные      299
Методы поиска вывода локальные      299
Минкер      10 269
Минус-нормализация      296
Минус-правила      296
Минц, Г.Е.      9 296 302 313 317
Множество атомов (atom set)      60 см. также Эрбрановский базис
Множество констант (constant set)      59
Множество констант поддержки (set of support)      111 219
Множество рассогласований (disagreement set)      82
Модальная логика (modal logic)      268
Модель в логике высказываний (model in propositional logic)      21
Модель в логике первого порядка (model in first-order logic)      42
Модифицированный метод поиска в глубину (modified depth-first method)      149
1 2 3
blank
Реклама
blank
blank
HR
@Mail.ru
       © Электронная библиотека попечительского совета мехмата МГУ, 2004-2024
Электронная библиотека мехмата МГУ | Valid HTML 4.01! | Valid CSS! О проекте