Mini-Workshop on Automated Deduction
Formal Digital Libraries and Little Engines of Proof
Mon/Tue Oct 27/28, 2003
EK255 SRI International, Menlo Park CA

We were recently awarded two medium NSF ITR (Information Technology Research) grants toward the goal of achieving more effective automation in applications of automated deduction. The Logosphere project is a collaborative effort between Yale University, Carnegie-Mellon University, and SRI International for developing formal digital libraries and supporting interoperation between different deductive frameworks. The Infer! project is a collaboration between SRI International, Clarkson University, and Pace University for building deductive middleware for defining, combining, and embedding inference procedures.

To kick off these projects and to explore synergies with other related efforts, we hosted a mini-workshop at SRI International in Menlo Park on Oct 27 and 28 (half day), 2003. The purpose of the workshop was to take stock of the research challenges confronting automated deduction and to coordinate responses to these challenges. The focus was on deductive engines, formalized libraries, and integration. The individual session will cover overviews of individual projects, a discussion of the opportunities for applications of automated deduction, the research challenges in developing and integrating libraries and tools, and the use of automated deduction in education.

The workshop organizers included Chris Lynch, Michael Kohlhase, Sam Owre, Frank Pfenning, Harald Ruess, Christelle Scharff, Carsten Schuermann, Natarajan Shankar, Ashish Tiwari

Mon Oct 27, 2003
9.00am Registration, Coffee
9.10am: N. Shankar: Welcome: Fact + Deduction = Insight!
9.20am: N. Shankar: Little Engines of Proof
9.40am: C. Lynch: Automatic Decidability
10.00: Discussion
10.20 COFFEE
10.40: C. Schuermann: Logosphere
11am: F. Pfenning: Proofs 'R Us
11.20: Discussion
11.40: G. Nelson: Performance Testing SIMPLIFY
12.00: C. Talcott: MAUDE
12.20: Discussion
12.30: Lunch
1.30 : S. Owre:
1.50 : R. Butler: Applications of Formal Libraries
2.10 : C. Brown: Proof Transformation
2.30 : B. di Vito: The Hypatheon Project
2.50 : R. Waldinger: Deductive Choreography
3.10 : Discussion
3.30 : Coffee
3.50 : H. Ruess: The Interface is the Message
4.10 : S. Berezin: CVC-Lite and Flyspec
4.30 : A. Tiwari: Qualitative Abstraction
4.50 : Sumit Gulwani: Join Algorithms: Theorem Proving Meets Program Analysis
5.10 : Discussion
5.30: CLOSE

7pm Dinner at Siam Gardens

Tue Oct 28, 2003
9.00: J. Millen: Crypto Protocol Verification
9.20: N. Shankar: Teaching Automated Deduction
9.40: C. Scharff: Creating Bridges
10.00: Discussion
10.20: COFFEE
10.40 : M. Beeson: Automated Deduction and Education
11.00 : R. Sommer: A Theorem Proving Environment for Teaching Mathematics
11.20: D. Espinosa: Category Theory as a Logical Framework
11.40: Discussion
noon: CLOSE