Главная    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
Предметный указатель
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
1 2 3
blank
Реклама
blank
blank
HR
@Mail.ru
       © Электронная библиотека попечительского совета мехмата МГУ, 2004-2024
Электронная библиотека мехмата МГУ | Valid HTML 4.01! | Valid CSS! О проекте