This volume constitutes the refereed proceedings of the 16th International Conference on Automated Deduction held in Italy in July 1999. It addresses recent issues in automated deduction and theorem proving, ranging from logical foundations to deduction systems design and evaluation.

Session 1.- A Dynamic Programming Approach to Categorial Deduction.- Tractable Transformations from Modal Provability Logics into First-Order Logic.- Session 2.- Decision Procedures for Guarded Logics.- A PSpace Algorithm for Graded Modal Logic.- Session 3.- Solvability of Context Equations with Two Context Variables Is Decidable.- Complexity of the Higher Order Matching.- Solving Equational Problems Efficiently.- Session 4.- VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up.- A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers.- Presenting Proofs in a Human-Oriented Way.- Session 5.- On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results.- Maslov’s Class K Revisited.- Prefixed Resolution: A Resolution Method for Modal and Description Logics.- Session 6: System Descriptions.- System Description: Twelf — A Meta-Logical Framework for Deductive Systems.- System Description: inka 5.0 - A Logic Voyager.- System Description: CutRes 0.1: Cut Elimination by Resolution.- System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving.- System Description Using OBDD’s for the Validationof Skolem Verification Conditions.- Fault-Tolerant Distributed Theorem Proving.- System Description: Waldmeister — Improvements in Performance and Ease of Use.- Session 7.- Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems.- A Formalization of Static Analyses in System F.- On Explicit Reflection in Theorem Proving and Formal Verification.- Session 8: System Descriptions.- System Description: Kimba, A Model Generator for Many-Valued First-Order Logics.- System Description:Teyjus—A Compiler and Abstract Machine Based Implementation of ?Prolog.- Vampire.- System Abstract: E 0.3.- Session 9.- Invited Talk: Rewrite-Based Deduction and Symbolic Constraints.- Towards an Automatic Analysis of Security Protocols in First-Order Logic.- Session 10.- A Confluent Connection Calculus.- Abstraction-Based Relevancy Testing for Model Elimination.- A Breadth-First Strategy for Mating Search.- Session 11: System Competitions.- The Design of the CADE-16 Inductive Theorem Prover Contest.- Session 12: System Descriptions.- System Description: Spass Version 1.0.0.- K : A Theorem Prover for K.- System Description: CYNTHIA.- System Description: MCS: Model-Based Conjecture Searching.- Session 13.- Embedding Programming Languages in Theorem Provers.- Extensional Higher-Order Paramodulation and RUE-Resolution.- Automatic Generation of Proof Search Strategies for Second-Order Logic.