|
|
 |
| Авторизация |
|
|
|
| Поиск по указателям |
|
|
|
|
|
|
|
 |
|
|
|
| Ben-Ari M — Mathematical Logic for Computer Science |
|
|
|
| Предметный указатель |
AND-OR tree 186
And-parallelism 188
Apt, K. 212 292
assertion 203
ASSIGNMENT 17 105
atom 13
Atom, ground 140
Axiom 27 43 48 61
Axiom, Gentzen system 45 62 128
Axiom, Hilbert system 48 60—61 129
Axiom, Hoare logic 210
Axiom, number theory 136
Axiom, temporal logic 257
Ben-Ari, M. 292
Binary decision diagram 81—95
Binary decision diagram, apply 86 90
Binary decision diagram, complexity 90
Binary decision diagram, definition 85
Binary decision diagram, implementation 92—95
Binary decision diagram, model checking 278
Binary decision diagram, ordered 89
Binary decision diagram, quantify 92 279
Binary decision diagram, reduce 83 89
Binary decision diagram, restrict 91 279
Boolean operator 2 9
Boolean operator, associativity 16 22
Boolean operator, commutativity 22
Boolean operator, conjunction 10
Boolean operator, disjunction 10
Boolean operator, equivalence 10
Boolean operator, exclusive or 10
Boolean operator, implication 10
Boolean operator, minimal set 23—24
Boolean operator, nand 10 23
Boolean operator, negation 9
Boolean operator, nor 10 23
Boolean operator, precedence 16
Boolean operator, principal operator 16
Bryant, R. 89—90 291
Cantor, G. 289
Cardinality 288
Cartesian product 287
Characteristic predicate 202
Church's Theorem 122
Church, A 121
Clausal form 68 142
Clause 68
Clause, clashing 71 152 164
Clause, empty 70
Clause, fact 176
Clause, goal 173 176
Clause, ground 142
Clause, guarded 192
Clause, Horn 176
Clause, parent 72 152
Clause, parity 97
Clause, program 176
Clause, subsume 70
Clause, unit 68
Clocksin, W. 292
Closed, atomically 33
Closure, existential 104
Closure, reflexive transitive 240 246 287
Closure, universal 104
co-NP=NP? 96
Compactness theorem, predicate calculus 121
Compactness theorem, propositional calculus 59
Completeness, Hoare logic 218
Completeness, predicate calculus, Gentzen system 128
Completeness, predicate calculus, Hilbert system 131
Completeness, predicate calculus, resolution 169
Completeness, predicate calculus, semantic tableaux 141
Completeness, predicate calculus, SLD-resolution 178
Completeness, propositional calculus, Gentzen system 47
Completeness, propositional calculus, Hilbert system 56—57
Completeness, propositional calculus, resolution 74—78
Completeness, propositional calculus, semantic tableaux 34—38
Completeness, relative 202
Completeness, strong 58
Completeness, temporal logic 262—264
complexity 95 99
Component graph 250 254
Computation rule 175
Conjunctive normal form 67
Consistency 57 136—137
Consistent see "Theory consistent"
Consistent, maximally 65
Constant 102
Constrain-and-generate 196
Cook, S. 96
Correct answer substitution 176
Creswell, M 292
De Morgan's laws 23 68
Decision procedure 25 43
Decision procedure, predicate calculus 102 112 121—124 153 165
Decision procedure, predicate calculus, solvable cases 124
Decision procedure, propositional calculus 25 34 100
Decision procedure, temporal logic 252
Deductive system 43
Derivation tree 13
Derived rule 48
Deterministic algorithm 95
Diller, A. 292
Disjunctive normal form 99
Domain 105 117 140 149 196 202 210 288
Dreben, B. 124 291
Duality 25 108 138 208 239 240 257 259 260
Eight-queens problem 194
Even, S. 250
Existential quantifier 103
Exponential time 95
Expression 154
Factoring 164
Failure node 75 169
Falsifiable predicate calculus 106
Falsifiable propositional calculus 24
Fitting, M. 291
Flip-flop 272 281
Formation tree 13
Formula, atomic 103
Formula, closed 104 106
Formula, complementary 30
Formula, condensable 125
Formula, future 241 250 260
Formula, ground 140
Formula, monadic 124
Formula, next 241
Formula, predicate calculus 103
Formula, propositional calculus 13
Formula, pure 120 124
Frame 241
Francez, N. 292
Fulfil 244 248 250 254
Function 139
Galil, Z. 291
Generalization see "Rule of inference generalization"
Generate-and-test 194
Gentzen system, Hauptsatz 64
Gentzen system, predicate calculus 127—128
Gentzen system, propositional calculus 45—48
Gentzen system, sequent 62
GHC 192—194
Goedel, K. 136
Goldbach's conjecture 5
Goldfarb, W. 124 291
Grammar 3 12
Gries, D. 291
Ground instance 140 142
Haken, A. 98
half-adder 3 99
| Harel, D. 291
Herbrand base 149
Herbrand interpretation 149
Herbrand model 149
Herbrand universe 148
Herbrand's theorem 150—151
Hilbert system, predicate calculus 129—135
Hilbert system, propositional calculus 48—59
Hilbert system, variants 60
Hilbert's program 2
Hintikka set, predicate calculus 117
Hintikka set, propositional calculus 36
Hintikka structure, temporal logic 243 247 248
Hintikka's lemma, predicate calculus 117
Hintikka's lemma, propositional calculus 37
Hintikka's lemma, temporal logic 249
Hoare logic 209—219
Hopcroft, J. 13 122
Horn clause 172
Hughes, G. 292
Huth, M. 63 266 291
Idempotent 22 171
Incompleteness theorem 136
Induction 290
Inference node 76 169
Instance 154
Integers 283
Interpretation, finitely presented 245
Interpretation, predicate calculus 105 140
Interpretation, propositional calculus 17
Interpretation, temporal logic 237
Intuitionistic logic 6
Invariant 206 211 263
Jaffar, J. 199 292
Lewis, H. 124 291
Lifting lemma 167
Lindenbaum's Lemma 137
Literal 30 113 124
Literal, complementary 30 72 152
Lloyd, J. 179 180 292
Logic programming 5 173—199
Logic programming, concurrent 186—194
Logic programming, constraint 194—199
Logical consequence 27 107
Logical equivalence 19 107
Loveland, D. 292
Lowenheim — Skolem theorem 121
Lowenheim's theorem 121
Lukasiewicz, J. 15
Maher, M. 199 292
Manna, Z. 267 277 292
Martelli, A. 292
Matrix 142
McMillan, K. 292
Mellish, C. 292
Mendelson, E. 61 124 134 136 291
Metalanguage 19
Minsky, M. 122
Modal logic 6 236
Model 24 26
Model checking 272—280
Model checking, implementation 279—280
Model checking, symbolic 277
Model, finite 112 120
Model, finitely presented 252
Model, predicate calculus 106
Model, temporal logic 238
modus ponens see "Rule of inference modus
Monk, D. 61 291
Montanari, U. 292
n-tuple 286
Natural deduction 63
Natural numbers 284
Nerode, A. 124 291
Nondeterministic algorithm 95
NP-complete 96
Object language 19
Olderog, E.-R. 212 292
Or-parallelism 188
P=NP? 96
Partial correctness 203 211
Peterson's algorithm 269 272
Pnueli, A. 267 277 292
Polish notation 15
Polynomial time 95
Postcondition 203 222
Potter, B. 292
Precondition 203 222
Predicate calculus 3 101—138
Predicate transformer 204
Prefix 124 142
Prenex conjunctive normal form 124 142
preorder traversal 14
Procedure 176
PROGRAM 202
Program specification 4
Program specification in Z 221
Program specification, concurrent 266—267
Program verification 4 211—213
Program verification, concurrent 269—272
Program, concurrent 266
Program, logic 176
Program, semantics 4 202—209
Program, synthesis 213—216
Programming language, CHIP 198
Programming language, CLP( ) 199
Programming language, PASCAL 4 5 104 205 269
Programming language, PROLOG 5 181—185
Programming language, Prolog, cut 184
Programming language, Prolog, non-logical predicate 183
proof 43
Proof checker, predicate calculus 134—135
Proof checker, propositional calculus 59—60
Propositional calculus 2 9—100
RANGE 288
Reductio ad absurdam see "Rule of inference reductio
Refutation 25 73 180
Relation 101 105 287
Renamable-Horn 172
renaming 71
Rescher, N. 292
Resolution 5
Resolution, general 164—169
Resolution, ground 152—153
Resolution, predicate calculus 139—172
Resolution, predicate calculus, implementation 170
Resolution, propositional calculus 67—80
Resolution, propositional calculus, complexity 96—98
Resolution, propositional calculus, implementation 78—80
Resolvent 72 152
Robinson, J. 67 153 159
Rule of inference 43
Rule of inference, C-Rule 133
Rule of inference, contrapositive 50
Rule of inference, cut 64
Rule of inference, deduction 49 130
Rule of inference, double negation 52
Rule of inference, exchange of antecedent 51
Rule of inference, generalization 129 257
Rule of inference, Gentzen system 45 62 128
Rule of inference, Hilbert system 129
Rule of inference, modus ponens 48 129 257
Rule of inference, modus tollens 64
Rule of inference, reductio ad absurdum 53
Rule of inference, structural induction 17
Rule of inference, temporal logic 257
Rule of inference, transitivity 51
Ryan, M. 63 266 291
Satisfiable predicate calculus 106
Satisfiable propositional calculus 24 26
|
|
|
| Реклама |
|
|
|
|
|
О проекте