| Time | Title | Place |
|---|
| 9:00-10:00 |
Session 11: Invited Talk |
Michael Kohlhase |
| 9:00-10:00 |
Logical Engineering with Instance-Based Methods (invited talk) |
Peter Baumgartner |
| 10:00-10:30 |
Coffee Break |
|
| 10:30-12:30 |
Session 12: Termination |
Gilles Dowek |
| 10:30-11:00 |
Predictive Labeling with Dependency Pairs using SAT |
Adam Koprowski, Aart Middeldorp |
| 11:00-11:30 |
Dependency Pairs for Rewriting with Non-Free Constructors |
Stephan Falke, Deepak Kapur |
| 11:30-12:00 |
Proving Termination by Bounded Increase |
J¨urgen Giesl, Ren´e Thiemann, Stephan Swiderski, Peter Schneider-Kamp |
| 12:00-12:30 |
Certified Size-Change Termination |
Alexander Krauss |
| 12:30-14:00 |
Lunch Break |
|
| 14:00-16:00 |
Session 13: Tableaux and First-Order Systems |
Hans de Nivelle |
| 14:00-14:30 |
Encoding First Order Proofs in SAT |
Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch,
Ralph Eric McGregor |
| 14:30-15:00 |
Hyper Tableaux with Equality |
Peter Baumgartner, Bj¨orn Pelzer, Ulrich Furbach |
| 15:00-15:15 |
System Description: E-KRHyper |
Bj¨orn Pelzer, Christoph Wernhard |
| 15:15-15:30 |
SPASS Version 30 |
Christoph Weidenbach, Renate Schmidt, Thomas Hillenbrand, Dalibor Topic, Rostislav Rusev |
| 15:30-16:00 |
SRASS-a Semantic Relevance Axiom Selection System |
Geoff Sutcliffe, Yury Puzis |