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

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

blank
blank
blank
Красота
blank
Troelstra A.S. — Basic proof theory
Troelstra A.S. — Basic proof theory

Читать книгу
бесплатно

Скачать книгу с нашего сайта нельзя

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



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


Название: Basic proof theory

Автор: Troelstra A.S.

Аннотация:

This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of first-order logic formalization. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic, logic programming theory, category theory, modal logic, linear logic, first-order arithmetic and second-order logic. In each case the authors illustrate the methods in relatively simple situations and then apply them elsewhere in much more complex settings. For the new edition, they have rewritten many sections to improve clarity, added new sections on cut elimination, and included solutions to selected exercises. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence.


Язык: en

Рубрика: Математика/

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

ed2k: ed2k stats

Издание: 1

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

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

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

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID
blank
Предметный указатель
2-sequent      216
Abstraction      9
Abstraction, type      291
Absurdity rule classical      31
Absurdity rule intuitionistic      31
Active formula      53
Aczel      107
Aczel slash      86 107
Adjacent inferences      124
Andreoii      199
Answer      181
Answer, computed      181
Answer, correct      181
Antecedent      53
Application      9
Application, simple      271
Application, type      291
Approximation theorem      239
APS      250
apt      197
Arithmetic, Heyting      151
Arithmetic, intuitionistic      151
Arithmetic, Peano      264
Arithmetic, primitive recursive      97—100
Arithmetical system      263
Arithmetical system, classical      264
Arithmetical system, intuitionistic      264
Arithmetical system, restricted      265
arrow      201
Arrow, identity      201
Arrow, truth      201
Arrow, variable      202
Assumption bound      32
Assumption cancelled      31
Assumption class      30
Assumption closed      31
Assumption discharged      31
Assumption eliminated      31
Assumption open      31
Assumption stability      41
Assumption variable      37
Atomic instances of axioms      56
AUTOMATH      49
Axiom 4-      226
Axiom axiom link      247
Axiom b-, c-, w-      35
Axiom K-      226
Axiom k-, s-      27
Axiom normality      226
Axiom T-      226
Baader      197
Babaev      223
Bachmann      260
Balanced formula      216
Barendregt      3 9 14 307
BCK-logic      234
Beeson      169
Belnap      257
Benthem, van      106
Benton      258
Bernays      48 106 285
Beth      74 106 107
Beth's definability theorem      91
BHK-interpretation      46
Bibel      73
Blyth      200
Boricic      170
Bottom-violation lemma      127 134
Bound assumption      32
Branch      8
Branch, main      147
Branching k-      8
Breazu — Tannen      307
Brouwer      29
Brouwer — Heyting — Koimogorov interpretation      46
Brouwer — Kleene ordering      283
Bruijn, de      3 49
Buchholz      136 284 285
Bull      255
c.c      294
Cancelled assumption      31
Candidate, computability      294
Cartesian closed category      203
Category      203
Category, cartesian closed      203
Category, free      204
Category, free cartesian closed      204
CCC      203
CCC, free      204
CDC      36 161
Cellucci      170 171
Chang      197
Church      48
Church numeral      18 291
Church — Rosser property      12
Church — Rosser property, weak      12
Class predicative      150
Clause      186
Clause formula      186
Clause formula, intuitionistic      190
Clause, initial      188
Clause, intuitionistic      190
Codomain of an arrow      201
Coherence theorem      216 223—224
Collapsing map      303
Colmerauer      197
Combinator      207
Combinator, $\wedge -$      207
Combinatory logic, typed      16
Complete discharge convention      36 161
Completeness for linear resolution      183
Completeness of resolution calculus      188
Completeness, combinatorial      18
Completeness, semantic      84
Complexity theory      136
Composition of arrows      201
Composition of substitutions      174
Comprehension, elementary      151
Computability candidate      294
Computability predicate      157 214
Conclusion of a link      247
Conclusion of a proof structure      247
Confluent      12
Confluent, weakly      12
Conjunction (object)      201
Conservative      7
Conservativity of definable functions      96 108
Consistency (of contexts)      34
Constructions, calculus of      307
context      5 34 53
Context, negative      5
Context, positive      5
Context, strictly positive      5
Context-free      55
Context-independent      55
Context-sharing      55
Contractible      11
Contraction      11 52
Contraction, $g\beta -$      142 163
Contraction, $\beta -$      12
Contraction, $\beta\eta -$      12
Contraction, $\eta -$      12
Contraction, $\exists - perm$      140
Contraction, $\exists -$      139
Contraction, $\forall -$      139
Contraction, $\rightarrow$      139
Contraction, $\vee - perm$      139
Contraction, $\vee -$      139
Contraction, $\wedge -$      139
Contraction, depth-preserving      67
Contraction, detour      139 289
Contraction, generalized $\beta -$      142 163
Contraction, permutation      139
Contraction, simplification      140
Contractum      11
Convertible      11
Coquand      307
CR      12
Craig      107
Critical cut      138
Curien      224
Curry      47 49 74 106—107 136 169 255 257
Currying operator      201
Cut      57 138
Cut elimination      76—83 229 240
Cut elimination, continuous      285
Cut elimination, generalizations of      97
Cut elimination, numerical bounds on      113—124
Cut link      247
Cut reduction lemma      113
Cut rule      57 106
Cut, additive      58
Cut, closure under      58 76—83
Cut, context-sharing      58
Cut, critical      138
Cut, critical g-      164
Cut, g-      163
Cutformula      57
Cutlevel      77
Cutrank      77 138 269
Dalen, van, ix, x      107
Danos      254 258
De Morgan duality      72 238
Decidability of Ip      86
Deduction      20
Deduction from hypotheses      6
Deduction graph      201
Deduction graph, positive      201
Deduction graph, tci-      201
Deduction Theorem      48
Deduction theorem, modal      227
Deduction variable      86 see “Definability” “Explicit”
Deduction, natural      20
Deduction, normal      138
Deduction, pure-variable      58
Definability theorem, Beth's      91
Depth (of a formula)      8
Depth of a tree      8
Derivation      20
Derivation, contractible      271
Derivation, normal      271
Derivation, quasi-normal      273
Detachment rule      49
Deviation reduction      220
Diller      170
Discharged assumption      31
Disjunction property      85 86
Doets      181 197
Domain of a substitution      174
Domain of an arrow      201
Dosen      89 257
Double negation law      42
Dragalin      57 74 81 106 306
Duality, De Morgan      72 238
Dyckhoff      109
E-logic      100—102
E-part      146
E-rule      30
Eisinger      197
Eliminated assumption      31
Elimination of empty succedent      56
Elimination part      146
Elimination rule      30
Elimination, cut      see “Cut elimination”
Embedding, Girard      242
Embedding, modal      230 256
Equality      11
Equivalent substitutions      175
Evaluation (arrow)      201
Ex-falso-quodlibet schema      264
Exchange rule      73
Excluded middle, law of      42
expansion      153
Explicit definability      86
Exponent object      201
f.o.      5
Fact      154
Faithfulness of modal embedding      233
Felscher      108 136
Fitting      106 109 111 255 257
Flagg      256
Formula clause      186
Formula occurrence      5
Formula occurrence, negative      5
Formula occurrence, positive      5
Formula occurrence, strictly positive      5
Formula, $\Pi_1 -$      264
Formula, active      53
Formula, balanced      216
Formula, cut      57
Formula, goal      178
Formula, Harrop      see “Rasiowa — Harrop”
Formula, hereditary Harrop      see “Hereditary Rasiowa — Harrop”
Formula, hereditary Rasiowa — Harrop      135
Formula, interpolation      90
Formula, main      53
Formula, negative      39
Formula, principal      53
Formula, Rasiowa — Harrop      86 107
Formula, side      53
Formulas-as-types      25 49 307
Fragment, negative      39
Free (for a variable)      3
Free cartesian closed category      204
Free category      204
Free CCC      204
Frege      48
Friedman      285 286 306
Fujiwara      108
function object      201
G (rule)      43
g-cut      163
g-cut, critical      164
Gallier      73 135 285 307
Gandy      169
Generalization rule      43
Gentzen system      52 55 65 73 74 100 102 109 189 228 229 236 237
Gentzen — Schuette system      71
Gentzen's method of cut elimination      81
Gentzen, ix      47—49 51 73 74 89 106 136 260 263 284 285
Geuvers      307
Girard embedding      242
Girard, ix      109 135 234 239 246 256—258 284 291 294 307 308
Glivenko      48
Goal      178
Goal formula      178
Goedel      49 169 255 256
Goodman      256
Gordeev      136 285
Gore      257
Graph deduction      201
Graph positive deduction      201
Graph tci-deduction      201
Hardin      224
Harland      198
Harrington      285
Harrop      107
Harrop formula      see “Rasiowa — Harrop hereditary” “Rasiowa
Headcut rule      243
Height of a tree      8
1 2 3
blank
Реклама
blank
blank
HR
@Mail.ru
       © Электронная библиотека попечительского совета мехмата МГУ, 2004-2019
Электронная библиотека мехмата МГУ | Valid HTML 4.01! | Valid CSS! О проекте