• Produktbild: Automated Deduction - CADE-16
  • Produktbild: Automated Deduction - CADE-16
Band 1632

Automated Deduction - CADE-16 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings

48,99 €

inkl. gesetzl. MwSt., Versandkostenfrei


Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

23.06.1999

Abbildungen

XIV, 438 p.

Herausgeber

Harald Ganzinger

Verlag

Springer Berlin

Seitenzahl

438

Maße (B/H)

15,5/23,5 cm

Gewicht

590 g

Auflage

1999

Sprache

Englisch

ISBN

978-3-540-66222-8

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

23.06.1999

Abbildungen

XIV, 438 p.

Herausgeber

Harald Ganzinger

Verlag

Springer Berlin

Seitenzahl

438

Maße (B/H)

15,5/23,5 cm

Gewicht

590 g

Auflage

1999

Sprache

Englisch

ISBN

978-3-540-66222-8

Herstelleradresse

Springer-Verlag GmbH
Heidelberger Platz 3
14197 Berlin
Deutschland
Email: sdc-bookservice@springer.com
Url: www.springer.com
Telephone: +49 30 827870
Fax: +49 30 8214091

Noch keine Bewertungen vorhanden

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.

Kundinnen und Kunden meinen

Bewertungen (0)

  • Produktbild: Automated Deduction - CADE-16
  • Produktbild: Automated Deduction - CADE-16
  • 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.