AY Journal of Automated Reasoning 23: 499, 1999. Author Index to Volume 23 Brodsky, A., 83 Naraschewski, W., 299 Nipkow, T., 299 Chou, C.-T., 265 Dubois, C., 319 Paulson; L.C., 235 Peled, D., 265 Goldschlag, D. M., 445 Pfening, F., 195 Pollack, R., 373 Hermann, M., 107 Jaume, M., 347 Ramsdell, J. D., 43 Recio, T., 63 Kammiiller, F., 235 Reus, B., 411 Kolaitis, P. G., 107 Rudnicki, P., 197 Kondo, H., 25 Kurihara, M., 25 Sutcliffe, G., | Suttner, C. B., | Lassez, C., 83 Lassez, J.-L., 83 Trybulec, A., 197 Maher, M. J., 83 Ménissier-Morain, V., 319 Van Gelder, A., 137 McKinna, J., 373 Vélez, M. P., 63 BS Jourof nAuatomlate d Reasoning 23: 501-502, 1999. Subject Index to Volume 23 associative-commutative matching , 107 lambda calculus, ; autarky, 137 LCF, 411 automated deduction, 107 LEGO proof checker, 373 automated theorem proving, automatic theorem proving, machine-checked proof, 299 Mini-ML, 299 Boolean formula, 137 MIZAR, 197 Boyer—Moore theorem prover, 43 ML, 319 model, 137 calculus of inductive constructions, model elimination, 137 319, 347 CEK machine, 43 NP-completeness, 107 competition, | completion, 25 parallelism, 445 PC-NQTHM, 445 computational complexity, 107 concurrency, 445 programming logics, 41] constraint databases, 83 propositional formula, 137 constraint programming, Pure Type Systems, 373 #P-completeness, 107 databases, 83 Diophantine equations, 107 QED Project. 197 domain theory, 411 refutation, 137 elementary geometry, 63 regular cardinals, 197 equational matching, 107 resolution, 137 equational reasoning, 25 satisfiability, 137 SECD machine, 43 formal mathematics, 373 semantics of logic programs, 347 formal proofs, 319, 347 set theory, 197 formal verification, 41 1 SLD-resolution, 347 Grobner basis, 63 spatial databases, 83 standardization apart, 347 Isabelle, 235 Sylow’s theorem, 235 Isabelle/HOL, 299 synthetic domain theory, 411 502 SUBJECT INDEX TO VOLUME 23 tail call, 43 type theory, 373, 411 tail recursion, 43 term rewriting, 25 Unity, 445 theorem proving, 137, 235, 445 verified implementation, 43 type inference, 299, 319 type system, 319 well-foundedness, 197