17. CADE 2000: Pittsburgh, PA, USA

Invited Talk

• John Harrison:
  High-Level Verification Using Theorem Proving and Formalized Mathematics. 1-6
  

Session 1:

• Neophytos G. Michael, Andrew W. Appel:
  Machine Instruction Syntax and Semantics in Higher Order Logic. 7-24
  
• George C. Necula, Peter Lee:
  Proof Generation in the Touchstone Theorem Prover. 25-44
  
• Konrad Slind:
  Wellfounded Schematic Definitions. 45-63
  

Session 2:

• Leo Bachmair, Ashish Tiwari:
  Abstract Congruence Closure and Specializations. 64-78
  
• Clark W. Barrett, David L. Dill, Aaron Stump:
  A Framework for Cooperating Decision Procedures. 79-98
  
• Florian Kammüller:
  Modular Reasoning in Isabelle. 99-114
  
• William M. Farmer:
  An Infrastructure for Intertheory Reasoning. 115-131
  

Session 3:

• Johan G. F. Belinfante:
  Gödel's Algorithm for Class Formation. 132-147
  
• Marc Bezem, Dimitri Hendriks, Hans de Nivelle:
  Automated Proof Construction in Type Theory Using Resolution. 148-163
  
• Peter B. Andrews, Matthew Bishop, Chad E. Brown:
  System Description: TPS: A Theorem Proving System for Type Theory. 164-169
  
• Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo:
  The Nuprl Open Logical Environment. 170-176
  
• Carsten Sinz:
  System Description: ARA - An Automatic Theorem Prover for Relation Algebras. 177-182
  

Invited Talk

• Henry A. Kautz:
  Scalable Knowledge Representation and Reasoning Systems. 183
  

Session 4:

• Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura:
  Efficient Minimal Model Generation Using Branching Lemmas. 184-199
  
• Peter Baumgartner:
  FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure. 200-219
  
• Ashish Tiwari, Leo Bachmair, Harald Rueß:
  Rigid E-Unification Revisited. 220-234
  

Invited Talk

• Carl-Johan H. Seger:
  Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice. 235
  

Session 5:

• E. Allen Emerson, Vineet Kahlon:
  Reducing Model Checking of the Many to the Few. 236-254
  
• Doron Bustan, Orna Grumberg:
  Simulation Based Minimization. 255-270
  
• Thomas Genet, Francis Klay:
  Rewriting for Cryptographic Protocol Verification. 271-290
  
• Enrico Giunchiglia, Armando Tacchella:
  System Description: *SAT: A Platform for the Development of Modal Decision Procedures. 291-296
  
• Peter F. Patel-Schneider:
  System Description: DLP. 297-301
  
• Gilles Audemard, Belaid Benhamou, Laurent Henocque:
  Two Techniques to Improve Finite Model Search. 302-308
  

Session 6:

• Jürgen Giesl, Aart Middeldorp:
  Eliminating Dummy Elimination. 309-323
  
• Deepak Kapur, Mahadevan Subramaniam:
  Extending Decision Procedures with Induction Schemes. 324-345
  
• Cristina Borralleras, Maria Ferreira, Albert Rubio:
  Complete Monotonic Semantic Path Orderings. 346-364
  

Session 7:

• Anatoli Degtyarev, Andrei Voronkov:
  Stratified Resolution. 365-384
  
• Bruce Spencer, Joseph Douglas Horton:
  Support Ordered Resolution. 385-400
  
• William McCune, Olga Shumsky:
  System Description: IVY. 401-405
  
• Geoff Sutcliffe:
  System Description: SystemOn TPTP. 406-410
  
• Marianne Brown, Geoff Sutcliffe:
  System Description: PTTP+GLiDes: Semantically Guided PTTP. 411-416
  

Session 8:

• Guillaume Gillard:
  A Formalization of a Concurrent Object Calculus up to alpha-Conversion. 417-432
  
• Renate A. Schmidt, Ullrich Hustadt:
  A Resolution Decision Procedure for Fluted Logic. 433-448
  
• Philippe Chatalic, Laurent Simon:
  ZRES: The Old Davis-Putman Procedure Meets ZBDD. 449-454
  
• Andreas Franke, Michael Kohlhase:
  System Description: MBASE, an Open Mathematical Knowledge Base. 455-459
  
• Andreas Meier:
  System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level. 460-464
  

Session 9:

• Viorica Sofronie-Stokkermans:
  On Unification for Bonded Distributive Lattices. 465-481
  
• Ian Horrocks, Ulrike Sattler, Stephan Tobies:
  Reasoning with Individuals for the Description Logic SHIQ. 482-496
  
• Graham Collins, Louise A. Dennis:
  System Description: Embedding Verification into Microsoft Excel. 497-501
  
• Michael Jackson, Helen Lowe:
  System Description: Interactive Proof Critics in XBarnacle. 502-506
  

Tutorials

• Carsten Schürmann:
  Tutorial: Meta-logical Frameworks. 507-508
  
• Stephen G. Pulman:
  Tutorial: Automated Deduction and Natural Language Understanding. 509-510
  
• Peter B. Andrews, Chad E. Brown:
  Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. 511-512
  

Workshops

• Peter Baumgartner, Christian G. Fermüller, Nicolas Peltier, Hantao Zhang:
  Workshop: Model Computation - Principles, Algorithms, Applications. 513
  
• Carsten Schürmann:
  Workshop: Automation of Proofs by Mathematical Induction. 514
  
• Didier Galmiche:
  Workshop: Type-Theoretic Languages: Proof-Search and Semantics. 515
  
• Erica Melis:
  Workshop: Automated Deduction in Education. 516
  
• Simon Colton, Volker Sorge, Ursula Martin:
  Workshop: The Role of Automated Deduction in Mathematics. 517