Авторизация
Поиск по указателям
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
Предметный указатель
Heijenoort, van 136 Heindorf, ix 106 Herbeiin 74 170 Herbrand 48 49 136 197 Herbrand's theorem 89 127 135 Hertz 106 Heyting 48 Hilbert system 42 48 226 239 Hilbert, ix 48 108 Hindley, x 9 49 223 Hintikka 74 106 Hirokawa 223 Hodas 198 199 Hodges 197 Horn clause 178 Horn clause, definite 178 Horn formula 154 Horn formula, definite 154 Horn formula, definite generalized 154 Horn formula, generalized 154 Howard 49 169 Hudelmaier 109 136 Hughes 255 Hyland 307 Hyperexponential function 115 Hypothesis of a proof structure 247 I-part 146 I-rule 30 Idempotent substitution 176 Identity arrow 201 Identity literal 2 IFF 2 IH 2 Implication (object) 201 Implication, linear 236 Induction, transfinite 259 Instance of a formula 274 Interpolant 90 Interpolation 90—96 107—108 255 258 Interpolation formula 90 Introduction part 146 Introduction rule 30 Intuitionistic logic 48 inversion 74 Inversion lemma 66 232 Inversion-rule strategy 116—124 Invertible rule 66 IPS 249 Isomorphism (of objects) 205 Jaeger 197 Jaskowski 47 223 Johannson 48 74 Joyal 223 K-axiom 226 Kalsbeek 197 Kanger 106 255 Kelly 223 Ketonen 74 106 108 Kleene's systems 70 Kleene, ix 48 70 73 106—108 136 286 Koimogorov 48 49 Kowalski 197 Kreisel 108 135 284 286 307 Kripke 106 257 Kuroda 49 l-rank 164 L-rule 52 Lambda calculus extensional simple typed 13 Lambda calculus polymorphic 291 Lambda calculus simple typed 13 Lambek 205 223 224 234 Lambek calculus 234 Law of Double Negation 42 Law of the excluded middle 42 Leaf 8 Leafsize 8 Left rule 52 Leivant 161 306 308 Lemma bottom-violation 127 134 Lemma cut reduction 113 Lemma inversion 66 74 232 Lemma local permutation 129 131 Lemma Newman's 13 Lemma substitution 10 Length of a branch 8 Length of a clause (formula) 186 Length of a formula 8 Length of a segment 138 Length of a tree 8 Letter, proposition 2 Level (of a cut) 77 Level of a derivation 268 Level of a formula 163 265 Level of an ordinal 260 Level, implication 163 Level-rank 164 Lewis 255 Lincoln 241 Linear implication 236 Linear logic 257 Linear logic, classical 237 Linear logic, intuitionistic 237 Linear resolution completeness for 183 Linear resolution soundness for 181 Link 247 Literal 188 Literal, negative 72 Literal, positive 71 Lloyd 197 Local permutation lemma 129 131 Lorenzen 74 Luckhardt 136 Lyndon 96 107 m.g.a. 176 m.g.u. 176 Maehara 108 256 Main formula 53 Major premise 31 Malmnas 107 Mann 224 Marker 30 Martelli 197 Martin — Loef 14 169 307 Martini 257 Maximal segment 138 McKinsey 256 McLarty 200 Metayer 258 Midcut rule 243 Midsequent theorem 136 Miller 198 Minimal logic 48 Minor premise 31 Mints 169 170 197 216 223 255—258 285 Modal embedding 230 256 Modal logic 255 modus ponens 43 Most general unifier 176 Motohashi 107 108 MP 43 Muiticut rule 82 Multicut 82 Multiple-conclusion natural deduction 170 Multiset 5 Nagashima 108 Natural deduction 20 47 Natural deduction in sequent style 34 Natural deduction system 29 Natural deduction, multiple-conclusion 170 Natural deduction, term calculus for 37 Necessitation rule 226 Nederpelt 49 Negative formula 39 Negative fragment 39 Negative literal 72 Negative translation 39 49 Negative translation, Goedel — Gentzen 40 Negative translation, Kolmogorov's 41 Negative translation, Kuroda's 42 Neumann 48 Newman 13 Newman's lemma 13 Node 8 Node, bottom 8 Node, top 8 Non-introduced 157 294 Non-sharing 55 normal 289 Normal deduction 138 Normal form 11 Normal form, unique 215 Normality axiom 226 Normalization 141 164 289 Normalization, bounds on 161—162 165—168 Normalization, strong 142 157 164 215 289 293 307 Normalizing, strongly 11 Numeral 263 Oberschelp 108 Object 201 Object, function 201 One-sided system 71 74 Ono 234 Order of a track 147 Order-restriction 126 129 Ordering theorem 127 131 135 Ordinal 260 Ordinal notation 260 Orevkov 170 Osswald 307 Paeppinghaus 307 PAR 236 Par link 247 Parentheses 3 Paris 285 Parsons 285 Part elimination 146 Part introduction 146 Part strictly positive 5 Partition, admissible 126 129 133 Peano arithmetic 279 Peano axioms 263 Peirce rule 47* Peirce's law 36 Permutable rules 124 194 Permutation contraction 139 Permutation rule 73 Permutation variable- 175 Pfenning 74 Pitts 109 Pohlers, ix 284 Poigne 200 Polymorphic lambda calculus 291 Polynomial 19 Polynomial, extended 19 Positive deduction graph 201 Positive literal 71 Pottinger 170 Prawitz 47 48 74 89 107 142 143 148 168—170 307 Pre-cut formula 164 Predecessor 8 Predecessor, immediate 8 Predicative class 150 Premise of a link 247 Premise, major 31 Premise, minor 31 Primitive recursive arithmetic 97—100 Principal formula 53 Product (object) 201 Program, definite 178 Progression rule 272 Progressive 265 proof 20 Proof structure 247 Proof structure, abstract 250 Proof structure, inductive 249 Proofnet 250 258 Prooftree 20 PS 247 PS, inductive 249 Pure-variable deduction 58 Pym 198 Query 178 R-rule 52 Rank (of a cut) 77 Rasiowa 107 256 Rasiowa — Harrop formula 86 Rasiowa — Harrop formula, hereditary 135 Rautenberg 255 Recursive functions, provably total 305 Redex 10 271 Redex, critical 164 Reduction 11 Reduction of strong normalization 160 Reduction sequence 11 Reduction tree 11 Reduction, deviation 220 Reduction, generated 11 Reduction, one-step 11 Reduction, proper 11 Reduction, weak 17 Redundant 218 Relevant unifier 176 renaming 3 Renardel de Lavalette 109 Representable 18 Resolution 197 Resolution calculus 191 258 Resolution derivation 180 Resolution derivation, unrestricted 179 Resolution rule 178 186 Resolution rule, unrestricted 178 Resolution system 186 Resultant 178 Reynolds 307 Right rule 52 Robinson 107 197 Ronchi della Rocca 258 Roorda 258 Root 8 rose 223 Rule Cut 57 106 Rule detachment 49 Rule exchange 73 Rule left 52 Rule Multicut 82 Rule P 47 Rule Peirce 47 Rule permutation 73 Rule progression 272 Rule right 52 s.p.p. 5 Sanchis 109 169 Scheilinx 256—258 Schroeder — Heister 171 Schuette, ix 74 106—108 284 285 Schulte — Moenting 108 Schwichtenberg 19 136 170 197 285 307 Scott 100 109 Second-order arithmetic, intuitionistic 300 Second-order extension, weak 151
Реклама
|
|
О проекте