Automated deduction–CADE 16 : 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999 : proceedings

Automated Deduction — CADE-16: 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings
Author: Harald Ganzinger
Published by Springer Berlin Heidelberg
ISBN: 978-3-540-66222-8
DOI: 10.1007/3-540-48660-7

Table 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