| Systems Session 1: Sunday 4th, 14:00-15:30 | |
|---|---|
| 14:00-15:00 | Invited Talk:
TBA Andrei Voronkov |
| 15:00-15:30 |
Darwin: A Theorem Prover for the Model Evolution Calculus Peter Baumgartner, Alexander Fuchs, Cesare Tinelli |
| | |
| Systems Session 2: Sunday 4th, 16:00-17:30 | |
| 16:00-16:30 |
Simple and Efficient Clause Subsumption with Feature Vector
Indexing Stephan Schulz |
| 16:30-17:00 |
Things to Know when Implementing LPO Bernd Löchner |
| 17:00-17:30 | Systems Panel:
Why do so few Theories have Empirically Successful Implementations -
do Theories need APIs? Stephan Schulz (Chair), Franz Baader, William McCune |
| | |
| Applications Session 1: Monday 5th, 09:00-10:30 | |
| 09:00-10:00 | Invited Talk:
Automated Reasoning in Perfect Developer David Crocker |
| 10:00-10:30 |
An Empirical Evaluation of Automated Theorem Provers in Software
Certification Ewen Denney, Bernd Fischer, Johann Schumann |
| | |
| Applications Session 2: Monday 5th, 11:00-12:30 | |
| 11:00-11:30 |
MoMM - Fast Interreduction and Retrieval in Large Libraries of
Formalized Mathematics Josef Urban |
| 11:30-12:00 |
Milestones for Automated Reasoning Larry Wos |
| 12:00-12:30 | Applications Panel:
Applications Developers' Wish Lists (for ATP) Simon Colton (Chair), David Crocker, Bernd Fischer |
| | |
| Demonstrations Session 1: Monday 5th, 14:00-15:30 | |
| 14:00-14:30 |
Otter-lambda, a Theorem Prover with Untyped Lambda Unification Michael Beeson |
| 14:30-15:00 |
Active Logic for More Effective Commonsense Reasoning Michael Anderson, Darsana Josyula, Don Perlis, Khemdut Purang |
| 15:00-15:30 |
Automated Theorem Provers in Software Certification Johannes Schumann, Ewen Denney, Bernd Fischer |
| | |
| Demonstrations Session 2: Monday 5th, 16:00-17:30 | |
| 16:00-17:00 |
ETPS Educational Theorem Proving System Peter B. Andrews |
| 17:00-17:30 | TBA TBA |
| | |