Overview

Full Product Details

Author:   Harald Ganzinger
Publisher:   Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
Imprint:   Springer-Verlag Berlin and Heidelberg GmbH & Co. K
Edition:   1999 ed.
Volume:   1632
Dimensions:   Width: 15.50cm , Height: 2.30cm , Length: 23.50cm
Weight:   1.390kg
ISBN:  

9783540662228

ISBN 10:   3540662227
Pages:   438
Publication Date:   23 June 1999
Audience:   Professional and scholarly ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   In Print  
This item will be ordered in for you from one of our suppliers. Upon receipt, we will promptly dispatch it out to you. For in store availability, please contact us.

Table of Contents

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.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions