Авторизация
Поиск по указателям
Troelstra A.S. — Basic proof theory
Обсудите книгу на научном форуме Нашли опечатку?
Название: 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.
Язык: Рубрика: Математика /Статус предметного указателя: Готов указатель с номерами страниц ed2k: ed2k stats Издание: 1Год издания: 1996Количество страниц: 353Добавлена в каталог: 02.11.2010Операции: Положить на полку |
Скопировать ссылку для форума | Скопировать ID
Предметный указатель
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, 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, 142 163 Contraction, 12 Contraction, 12 Contraction, 12 Contraction, 140 Contraction, 139 Contraction, 139 Contraction, 139 Contraction, 139 Contraction, 139 Contraction, 139 Contraction, depth-preserving 67 Contraction, detour 139 289 Contraction, generalized 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, 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
Реклама
|
|
О проекте