Automated Deduction - CADE-17

17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000. Proceedings

  • David McAllester
Conference proceedings CADE 2000

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

Also part of the Lecture Notes in Artificial Intelligence book sub series (LNAI, volume 1831)

Table of contents

  1. Front Matter
  2. Invited Talk:

  3. Session 1:

    1. Neophytos G. Michael, Andrew W. Appel
      Pages 7-24
    2. George C. Necula, Peter Lee
      Pages 25-44
    3. Konrad Slind
      Pages 45-63
  4. Session 2:

    1. Leo Bachmair, Ashish Tiwari
      Pages 64-78
    2. Clark W. Barrett, David L. Dill, Aaron Stump
      Pages 79-98
    3. Florian Kammüller
      Pages 99-114
    4. William M. Farmer
      Pages 115-131
  5. Session 3:

    1. Johan Gijsbertus Frederik Belinfante
      Pages 132-147
    2. Marc Bezem, Dimitri Hendriks, Hans de Nivelle
      Pages 148-163
    3. Peter B. Andrews, Matthew Bishop, Chad E. Brown
      Pages 164-169
    4. Stuart F. Allen, Robert L. Constable, Rich Eaton, Christoph Kreitz, Lori Lorigo
      Pages 170-176
  6. Invited Talk:

  7. Session 4:

    1. Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura
      Pages 184-199
    2. Ashish Tiwari, Leo Bachmair, Harald Ruess
      Pages 220-234
  8. Invited Talk:

  9. Session 5:

    1. E. Allen Emerson, Vineet Kahlon
      Pages 236-254
    2. Doron Bustan, Orna Grumberg
      Pages 255-270
    3. Thomas Genet, Francis Klay
      Pages 271-290
    4. Peter Patel-Schneider
      Pages 297-301
    5. Gilles Audemard, Belaid Benhamou, Laurent Henocque
      Pages 302-308
  10. Session 6:

    1. Jürgen Giesl, Aart Middeldorp
      Pages 309-323
    2. Deepak Kapur, Mahadavan Subramaniam
      Pages 324-345
    3. Cristina Borralleras, Maria Ferreira, Albert Rubio
      Pages 346-364
  11. Session 7:

    1. Anatoli Degtyarev, Andrei Voronkov
      Pages 365-384
    2. Bruce Spencer, Joseph D. Horton
      Pages 385-400
    3. William McCune, Olga Shumsky
      Pages 401-405
    4. Geoff Sutcliffe
      Pages 406-410
    5. Marianne Brown, Geoff Sutcliffe
      Pages 411-416
  12. Session 8:

  13. Session 9:

    1. Viorica Sofronie-Stokkermans
      Pages 465-481
    2. Ian Horrocks, Ulrike Sattler, Stephan Tobies
      Pages 482-496
    3. Graham Collins, Louise A. Dennis
      Pages 497-501
    4. Mike Jackson, Helen Lowe
      Pages 502-506
  14. Tutorials:

  15. Workshops:

    1. Peter Baumgartner, Chris Fermueller, Nicolas Peltier, Hantao Zhang
      Pages 513-513
    2. Erica Melis
      Pages 516-516
    3. Simon Colton, Volker Sorge, Ursula Martin
      Pages 517-517

About these proceedings


For the past 25 years the CADE conference has been the major forum for the presentation of new results in automated deduction. This volume contains the papers and system descriptions selected for the 17th International Conference on Automated Deduction, CADE-17, held June 17-20, 2000,at Carnegie Mellon University, Pittsburgh, Pennsylvania (USA). Fifty-three research papers and twenty system descriptions were submitted by researchers from ?fteen countries. Each submission was reviewed by at least three reviewers. Twenty-four research papers and ?fteen system descriptions were accepted. The accepted papers cover a variety of topics related to t- orem proving and its applications such as proof carrying code, cryptographic protocol veri?cation, model checking, cooperating decision procedures, program veri?cation, and resolution theorem proving. The program also included three invited lectures: “High-level veri?cation using theorem proving and formalized mathematics” by John Harrison, “Sc- able Knowledge Representation and Reasoning Systems” by Henry Kautz, and “Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice” by Carl Seger. Abstracts or full papers of these talks are included in this volume.In addition to the accepted papers, system descriptions, andinvited talks, this volumecontains one page summaries of four tutorials and ?ve workshops held in conjunction with CADE-17.


Automat Resolution automated deduction model checking proving theorem proving verification

Editors and affiliations

  • David McAllester
    • 1
  1. 1.Toyota Technological Institute at ChicagoChicago

Bibliographic information

  • DOI
  • Copyright Information Springer-Verlag Berlin Heidelberg 2000
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Springer Book Archive
  • Print ISBN 978-3-540-67664-5
  • Online ISBN 978-3-540-45101-3
  • Series Print ISSN 0302-9743
  • Series Online ISSN 1611-3349
  • Buy this book on publisher's site
Industry Sectors
Materials & Steel
Chemical Manufacturing
Finance, Business & Banking
IT & Software
Consumer Packaged Goods
Energy, Utilities & Environment
Oil, Gas & Geosciences