Automated Deduction - CADE-16: 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings [Paperback]

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.- Maslovs 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 OBDDs 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:TeyjusA 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 AnalysilÓx