CADE-17   Carnegie Mellon University - School of Computer Science


David McAllester, Program Chair

Events are held in the University Center unless otherwise noted. The main events are in McConomy Auditorium, registration and breaks in the adjacent Connan Room. Lunch is downstairs in Rangos Hall. Workshops, tutorials, and system competition will be held in Wean Hall. System demonstrations will be in the break following the 10-minute system presentation in a room near McConomy Auditorium.

The banquet will be held at the Pittsburgh Golf Club, which is located adjacent to the Carnegie Mellon Campus, about a 5 minute walk away from the University Center.

Friday, June 16: Workshops and Tutorials
7:00-9:00 Welcome Reception, Connan Room, UC

Saturday, June 17

8:45 Opening Remarks: Ulrich Furbach, President of CADE
9:00 Invited Talk: High-Level Verification Using Theorem Proving and Formalized Mathematics
  John Harrison
10:00 CASC Entrants' Meeting, Connan Room, UC
  Followed by System Competition, 5th Floor Cluster, Wean Hall
10:00 Coffee Break
10:30 Machine Instruction Syntax and Semantics in Higher Order Logic
  Neophytos G. Michael and Andrew Appel
11:00 Proof Generation in the Touchstone Theorem Prover
  George C. Necula and Peter Lee
11:30 Wellfounded Schematic Definitions
  Konrad Slind
12:00 Lunch
1:30 Abstract Congruence Closure and Specializations
  Leo Bachmair and Ashish Tiwari
2:00 A Framework for Cooperating Decision Procedures
  Clark W. Barrett, David L. Dill, and Aaron Stump
2:30 Modular Reasoning in Isabelle
  Florian Kammuller
3:00 An Infrastructure for Intertheory Reasoning
  William Farmer
3:30 Break
4:00 Godel's Algorithm for Class Formation
  Johan Gijsbertus Frederik Belinfante
4:30 Automated Proof Construction in Type Theory using Resolution
  Marc Bezem, Dimitri Hendriks and Hans de Nivelle
5:00 System: TPS, A Theorem Proving System for Type Theory
  Peter B. Andrews, Matthew Bishop and Chad E. Brown
5:10 System: The Nuprl Open Logical Environment
  S. F. Allen, R. L. Constable, R. Eaton, C. Kreitz and L. Lorigo
5:20 System: ARA - An Automatic Theorem Prover for Relation Algebras
  Carsten Sinz
5:30 End of Session

Sunday June 18

8:45 Invited Talk: Scalable Knowledge Representation and Reasoning Systems
  Henry Kautz
9:45 Coffee Break
10:00 Efficient Minimal Model Generation Using Branching Lemmas
  Ryuzo Hasegawa, Hiroshi Fujita, and Miyuki Koshimura
10:30 FDPLL --- A First Order Davis-Putnam-Loveland Procedure
  Peter Baumgartner
11:00 Rigid E-Unification Revisited
  A. Tiwari, L. Bachmair, and H. Ruess
11:30 Break
12:00 Excursion Buses Leave from University Center
6:00 Return from Excursion
7:30 Banquet, Pittsburgh Golf Club

Monday, June 19

8:45 Invited Talk: Connecting Bits with Floating-Point Numbers:
  Model Checking and Theorem Proving in Practice
  Carl Seger
9:45 Coffee Break
10:15 Reducing Model Checking of the Many to the Few
  E. Allen Emerson and Vineet Kahlon
10:45 Simulation Based Minimization
  Doron Bustan and Orna Grumberg
11:15 Rewriting for Cryptographic Protocol Verification
  Thomas Genet and Francis Klay
11:45 System: *SAT, A Platform for the Development of Modal Decision Procedures
  Enrico Giunchiglia and Armando Tacchella
11:55 System: DLP
  Peter F. Patel-Schneider
12:05 System: Two Techniques to Improve Finite Model Search
  Audemard Gilles, Benhamou Belaid, Henocque Laurent
12:15 Lunch
1:15 CADE Business Meeting
2:00 Eliminating Dummy Elimination
  Jurgen Giesl and Aart Middeldorp
2:30 Extending Decision Procedures with Induction Schemes
  Deepak Kapur and M. Subramaniam
3:00 Complete Monotonic Semantic Path Orderings
  Cristina Borralleras, Maria Ferreira and Albert Rubio
3:30 Break
4:00 Stratified Resolution
  Anatoli Degtyarev and Andrei Voronkov
4:30 Support Ordered Resolution
  Bruce Spencer and J. D. Horton
5:00 System: IVY
  William McCune and Olga Shumsky
5:10 System: SystemOnTPTP
  Geoff Sutcliffe
5:20 System: PTTP+GLiDes, Semantically Guided PTTP
  Marianne Brown and Geoff Sutcliffe
5:30 End of Session
6:00 CASC Result Presentation
  Geoff Sutcliffe and Division Winners
6:30 CASC Panel Discussion

Tuesday, June 20

8:45 A Formalization of a Concurrent Object Calculus up to Alpha-Conversion
  Guillaume Gillard
9:15 A Resolution Decision Procedure for Fluted Logic
  Renate A. Schmidt and Ullrich Hustadt
9:45 System: ZRes: Meeting of the Old Davis-Putnam procedure with ZBDD
  Philippe Chatalic and Laurent Simon
9:55 System: MBase and Open Mathematical Knowledge Base
  Andreas Franke and Michael Kohlhase
10:05 System: TRAMP: Proof Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level
  Andreas Meier
10:15 Break
10:45 On Unification for Bounded Distributive Lattices
  Viorica Sofronie-Stokkermans
11:15 Reasoning with Individuals for the Description Logic SHIQ
  Ian Horrocks, Ulrike Sattler and Stephan Tobies
11:45 System: Embedding Verification into Microsoft Excel
  Graham Collins and Louise A. Dennis
11:55 System: Interactive Proof Critics in XBarnacle
  Helen Lowe and Mike Jackson
12:05 End of CADE Technical Program
12:15 Lunch
Afternoon: Workshops and Tutorials

Wednesday, June 21, Morning: Workshops

[ Home | Program | Workshops | Tutorials | System Competition ]
[ Accommodations | Excursions | Computing Facilities | Athletic Facilities | Restaurants | Travel ]
[ On-Line Registration ]        [ UNIF 2000 ]
Contact Us