Automated Deduction — CADE-16: 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 ProceedingsAuthor: Harald Ganzinger Published by Springer Berlin Heidelberg ISBN: 978-3-540-66222-8 DOI: 10.1007/3-540-48660-7Table of Contents:A Dynamic Programming Approach to Categorial Deduction Tractable Transformations from Modal Provability Logics into First-Order Logic Decision Procedures for Guarded Logics A PSpace Algorithm for Graded Modal Logic Solvability of Context Equations with Two Context Variables Is Decidable Complexity of the Higher Order Matching Solving Equational Problems Efficiently 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 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 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, Includes bibliographical references and index