04557oam 2200553 450 991014346130332120210716122944.03-540-48660-710.1007/3-540-48660-7(CKB)1000000000211087(SSID)ssj0000321525(PQKBManifestationID)11231244(PQKBTitleCode)TC0000321525(PQKBWorkID)10279477(PQKB)10761684(DE-He213)978-3-540-48660-2(MiAaPQ)EBC3073361(MiAaPQ)EBC6486271(PPN)155176625(EXLCZ)99100000000021108720210716d1999 uy 0engurnn|008mamaatxtccrAutomated deduction - CADE-16 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, proceedings /Harald Ganzinger (Ed.)1st ed. 1999.Berlin ;Heidelberg :Springer,[1999]©19991 online resource (XIV, 438 p.) Lecture Notes in Computer Science ;1632Bibliographic Level Mode of Issuance: Monograph3-540-66222-7 Includes bibliographical references at the end of each chapters and index.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.Lecture notes in computer science ;1632.Automatic theorem provingCongressesAutomatic theorem proving004.015113Ganzinger HaraldInternational Conference on Automated DeductionMiAaPQMiAaPQUtOrBLWBOOK9910143461303321Automated deduction - CADE-162106940UNINA