|
|
 |
| Авторизация |
|
|
|
| Поиск по указателям |
|
|
|
|
|
|
|
 |
|
|
|
| Ben-Ari M — Mathematical Logic for Computer Science |
|
|
|
| Предметный указатель |
Satisfiable temporal logic 238
Schneider, F. 291
Scope of variable 103
Search rule 175 180
Self-fulfilling 251 254
Semantic tableau, clauses 150
Semantic tableau, predicate calculus 109—120
Semantic tableau, predicate calculus, completeness 118
Semantic tableau, predicate calculus, implementation 118—120
Semantic tableau, predicate calculus, systematic 113
Semantic tableau, propositional calculus 29—40
Semantic tableau, propositional calculus, implementation 38—40
Semantic tableau, specification in Z 230—233
Semantic tableau, temporal logic 242—252
Semantic tableau, temporal logic, implementation 252—255
Semantic tableau, temporal logic, model checking 275
Semantic tree 74
Semi-decision procedure 151
Set 283
Set, complement 285
Set, countable 112 121 288
Set, difference 285
Set, disagreement 160
Set, disjoint 285
Set, element 283
Set, empty 283
Set, intersection 285
Set, operator 284
Set, ordered 286
Set, powerset 289
Set, proper subset 284
Set, subset 284
Set, uncountable 288
Set, union 285
Shannon expansion 91
Shapiro, E. 292
Shore, R. 124 291
Sinclair, J. 292
Singh, S. viii
Skolem function 144
Skolem's theorem 143—146
Skolemization algorithm 144—145
Skolemization algorithm, implementation 146—148
SLD-resolution 176—181
SLD-resolution, backtrack point 182
SLD-tree 180
Smullyan, R. 1 7 58 64 136 291
Soundness, Hoare logic 218
Soundness, predicate calculus, Gentzen system 128
Soundness, predicate calculus, Hilbert system 131
Soundness, predicate calculus, resolution 169
Soundness, predicate calculus, semantic tableaux 114—115
Soundness, predicate calculus, SLD-resolution 178
Soundness, propositional calculus, Gentzen system 47
Soundness, propositional calculus, Hilbert system 56
Soundness, propositional calculus, resolution 74
Soundness, propositional calculus, semantic tableaux 34—35
Soundness, temporal logic 262
Spivey, M. 292
Standardizing apart 164
State path 246
State transition diagram 237
Statman, R. 292
Sterling, L. 292
Strongly connected component 250 254
Structural induction see "Rule of inference structural
Structure 246
| Subformula 20
Substitution, composition 154
Substitution, instance 238 257
Substitution, predicate calculus 153
Substitution, propositional calculus 20
Syllogism 1
Tautology 24
Temporal logic 6 235—281
Temporal logic, branching-time 240 265 277
Temporal logic, linear-time 240
Temporal logic, models of time 239—242
Temporal logic, operators 236 264—266
Temporal logic, past 265
Temporal logic, precedence 264
Term 139
Term, equation 156
Term, ground 140
Theorem 27
Theorem proving 5
Theorems on weakest precondition 208—209
Theory 27
Theory, complete 135
Theory, decidable 137
Theory, effectively axiomatizable 137
Theory, number 136
Theory, set 283—290
Till, D. 292
Total correctness 212
Truth table 25 81
Truth table, complexity 95
Truth value 17
Tseitin, G. 98
Turing machine 122
Turing, A. 121
Two-register machine 122
Ullman, J. 13 122
Undecidability, predicate calculus 122—124
Undecidability, Prolog programs 124
Unification 155—163
Unification, algorithm 156—159
Unification, algorithm, implementation 161—163
Unification, occur check 156 161
Unification, Robinson's algorithm 160
Unifier 155
Universal quantifier 103
Unsatisfiable 26
Unsatisfiable predicate calculus 106
Unsatisfiable propositional calculus 24
Urquhart, A. 98 291 292
Valid predicate calculus 106
Valid propositional calculus 24
Valid temporal logic 238
Value of formula 105
Van Hentenryck, P. 194 292
Variable 102
Variable, bound 104
Variable, change of bound 133
Variable, free 104
Variable, quantified 103
Velleman, D. 43 283 291
Venn diagram 284
Weakest precondition 204
Weakest precondition of statements 205—208
Well-founded set 213
Wiles, A. viii
Wos, L. 292
Z 221—234
|
|
|
| Реклама |
|
|
|
|
|
О проекте