Skip to main content
SpringerLink
Log in
Book cover

Automated Deduction - CADE-16

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

  • Conference proceedings
  • © 1999

Overview

Authors:
  1. Harald Ganzinger

    1. Max-Planck-Institut für Informatik, Saarbrücken, Germany

    View author publications

    You can also search for this author in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 1632)

Part of the book sub series: Lecture Notes in Artificial Intelligence (LNAI)

Included in the following conference series:

Conference proceedings info: CADE 1999.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (40 papers)

  1. Front Matter

    Pages I-XIV
    Download chapter PDF

  3. Session 2

    1. Decision Procedures for Guarded Logics

      • Erich Grädel
      Pages 31-51

    2. A PSpace Algorithm for Graded Modal Logic

      • Stephan Tobies
      Pages 52-66

  4. Session 3

    1. Solvability of Context Equations with Two Context Variables Is Decidable

      • Manfred Schmidt-Schauß, Klaus U. Schulz
      Pages 67-81

    2. Complexity of the Higher Order Matching

      • ToMasz Wierzbicki
      Pages 82-96

    3. Solving Equational Problems Efficiently

      • Reinhard Pichler
      Pages 97-111

  5. Session 4

    1. VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up

      • A. A. Adams, H. Gottliebsen, S. A. Linton, U. Martin
      Pages 112-126

    2. A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers

      • Predrag Janičić, Alan Bundy, Ian Green
      Pages 127-141

    3. Presenting Proofs in a Human-Oriented Way

      • Helmut Horacek
      Pages 142-156

  6. Session 5

    1. On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results

      • Viorica Sofronie-Stokkermans
      Pages 157-171

    2. Maslov’s Class K Revisited

      • Ullrich Hustadt, Renate A. Schmidt
      Pages 172-186

    3. Prefixed Resolution: A Resolution Method for Modal and Description Logics

      • Carlos Areces, Hans de Nivelle, Maarten de Rijke
      Pages 187-201

  7. Session 6: System Descriptions

    1. System Description: Twelf — A Meta-Logical Framework for Deductive Systems

      • Frank Pfenning, Carsten Schürmann
      Pages 202-206

    2. System Description: inka 5.0 - A Logic Voyager

      • Serge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer
      Pages 207-211

    3. System Description: CutRes 0.1: Cut Elimination by Resolution

      • Matthias Baaz, Alexander Leitsch, Georg Moser
      Pages 212-216

    4. System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving

      • Andreas Franke, Michael Kohlhase
      Pages 217-221

    5. System Description Using OBDD’s for the Validationof Skolem Verification Conditions

      • E. Pascal Gribomont, Nachaat Salloum
      Pages 222-226

    6. Fault-Tolerant Distributed Theorem Proving

      • Jason Hickey
      Pages 227-231
Back to top

Other volumes

  1. Automated Deduction — CADE-16

Keywords

Authors and Affiliations

  • Max-Planck-Institut für Informatik, Saarbrücken, Germany

    Harald Ganzinger

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation