a Journal of Automated Reasoning 27: 423, 2001. Author Index to Volume 27 Basin, D., 1 Littman, M.L., 2 Bittencourt, G., 353 Lue: 4. 3 Bognar, M., 29 Bonatti, P. A., 391 Majercik, S.M., 2 Callaghan, P., 3 PitassiT,. , 251 De Vrijer, R., 29 Severi, P., 61 Sutcliffe, G., 227 Felty, A., 1 Szasz, N., 61 Fiorino, G., 297 Fitelson, B., 141, 201 Tonin, I., 353 Gamboa, R. A., 323 Ulrich, D., 97 Harris, K., 141 He, L., 313 Veroff, R., 123, 157 Kaufmann, M., 323 Wos, L., 89, 175, 201 ae Journal of Automated Reasoning 27: 425, 2001. Subject Index to Volume 27 artificial intelligence, 251 missing proofs, 201 automated reasoning, 89, 97, 175, 201 model generation theorem proving, 313 automated theorem proving, 227 nonstandard analysis, 323 automated theorem proving with the reals, 323 open problems, 97 competition, 227 pretyping, 29 condensed detachment, 97, 123, 157 probability theory, 251 context calculus, 29 program extraction, 61 proof finding, 89 detachment, 97, 141 proof sketch, 157 distributivity, 141 propositional calculus, 175 double negation, 175 dual transformation, 353 resolution, 391 Dummett logic, 297 SATCHMO, 313 elegant proofs, 89 satisfiability, 251 sentential, 141 first-order logic, 353 sentential calculi, 97 floundering, 391 shortest proofs, 123 formal proofs, 97 single axioms, 97 forward chaining, 313 skeptical derivations, 391 hints, 157 stable semantics, 391 strategies, 39] implementation, 3 substructural, 141 intelligent backtracking, 313 tableau calculus, 297 lambda calculus, 29 term-avoidance proofs, 201 linked UR-resolution, KZ, 1357 theorem proving, 353 logic, 89, 97, 141 theory of Specifications, 61 logical framework, 3 two-valued sentential calculus, 175 Lukasiewicz, 141 type theory, 3, 61 Meredith single axiom, 175 universes, 3