LEADER 04557oam 2200553 450 001 9910143461303321 005 20210716122944.0 010 $a3-540-48660-7 024 7 $a10.1007/3-540-48660-7 035 $a(CKB)1000000000211087 035 $a(SSID)ssj0000321525 035 $a(PQKBManifestationID)11231244 035 $a(PQKBTitleCode)TC0000321525 035 $a(PQKBWorkID)10279477 035 $a(PQKB)10761684 035 $a(DE-He213)978-3-540-48660-2 035 $a(MiAaPQ)EBC3073361 035 $a(MiAaPQ)EBC6486271 035 $a(PPN)155176625 035 $a(EXLCZ)991000000000211087 100 $a20210716d1999 uy 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 00$aAutomated deduction - CADE-16 $e16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, proceedings /$fHarald Ganzinger (Ed.) 205 $a1st ed. 1999. 210 1$aBerlin ;$aHeidelberg :$cSpringer,$d[1999] 210 4$d©1999 215 $a1 online resource (XIV, 438 p.) 225 1 $aLecture Notes in Computer Science ;$v1632 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-66222-7 320 $aIncludes bibliographical references at the end of each chapters and index. 327 $aSession 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. 410 0$aLecture notes in computer science ;$v1632. 606 $aAutomatic theorem proving$vCongresses 615 0$aAutomatic theorem proving 676 $a004.015113 702 $aGanzinger$b Harald 712 12$aInternational Conference on Automated Deduction 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bUtOrBLW 906 $aBOOK 912 $a9910143461303321 996 $aAutomated deduction - CADE-16$92106940 997 $aUNINA