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

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.