Automated Deduction - CADE-16: 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings (Lecture Notes in Computer Science, 1632)

This Book Constitutes The Refereed Proceedings Of The 16th International Conference On Automated Deduction, Cade-16, Held In Trento, Italy In July 1999 As Part Of Floc'99. The 21 Revised Full Papers Presented Were Carefully Reviewed And Selected From A Total Of 83 Submissions. Also Included Are 15 System Descriptions And Two Invited Full Papers. The Book Addresses All Current Issues In Automated Deduction And Theorem Proving, Ranging From Logical Foundations To Deduction Systems Design And Evaluation. A Dynamic Programming Approach to Categorial Deduction....Pages 1-15 Tractable Transformations from Modal Provability Logics into First-Order Logic....Pages 16-30 Decision Procedures for Guarded Logics....Pages 31-51 A PSpace Algorithm for Graded Modal Logic....Pages 52-66 Solvability of Context Equations with Two Context Variables Is Decidable....Pages 67-81 Complexity of the Higher Order Matching....Pages 82-96 Solving Equational Problems Efficiently....Pages 97-111 VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up....Pages 112-126 A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers....Pages 127-141 Presenting Proofs in a Human-Oriented Way....Pages 142-156 On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results....Pages 157-171 Maslov’s Class K Revisited....Pages 172-186 Prefixed Resolution: A Resolution Method for Modal and Description Logics....Pages 187-201 System Description: Twelf — A Meta-Logical Framework for Deductive Systems....Pages 202-206 System Description: inka 5.0 - A Logic Voyager....Pages 207-211 System Description: CutRes 0.1: Cut Elimination by Resolution....Pages 212-216 System Description: MathWeb , an Agent-Based Communication Layer for Distributed Automated Theorem Proving....Pages 217-221 System Description Using OBDD’s for the Validationof Skolem Verification Conditions....Pages 222-226 Fault-Tolerant Distributed Theorem Proving....Pages 227-231 System Description: Waldmeister — Improvements in Performance and Ease of Use....Pages 232-236 Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems....Pages 237-251 A Formalization of Static Analyses in System F ....Pages 252-266 On Explicit Reflection in Theorem Proving and Formal Verification....Pages 267-281 System Description: Kimba, A Model Generator for Many-Valued First-Order Logics....Pages 282-286 System Description: Teyjus—A Compiler and Abstract Machine Based Implementation of λProlog....Pages 287-291 Vampire....Pages 292-296 System Abstract: E 0.3....Pages 297-301 Invited Talk: Rewrite-Based Deduction and Symbolic Constraints....Pages 302-313 Towards an Automatic Analysis of Security Protocols in First-Order Logic....Pages 314-328 A Confluent Connection Calculus....Pages 329-343 Abstraction-Based Relevancy Testing for Model Elimination....Pages 344-358 A Breadth-First Strategy for Mating Search....Pages 359-373 The Design of the CADE-16 Inductive Theorem Prover Contest....Pages 374-377 System Description: Spass Version 1.0.0....Pages 378-382 K : A Theorem Prover for K....Pages 383-387 System Description: CYNTHIA ....Pages 388-392 System Description: MCS: Model-Based Conjecture Searching....Pages 393-397 Embedding Programming Languages in Theorem Provers....Pages 398-398 Extensional Higher-Order Paramodulation and RUE-Resolution....Pages 399-413 Automatic Generation of Proof Search Strategies for Second-Order Logic....Pages 414-428 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. Modern categorial grammars [8], which are intended to give a deductive account of grammatical composition, are based on substructural logics whose paradigm is the Lambek calculus [7].