| Speaker | Paper | System |
|---|---|---|
| Ben | Theorem Proving via General Matings | Otter |
| Chris | Semantic Tableaux | E |
| George | The Search Efficiency of Theorem Proving Strategies | Otter |
| Haiou | FDPLL--A First-Order Davis-Putnam-Logeman-Loveland Procedure | Vampire |
| Joiey | Eliminating Duplication in the Hyper-linking Strategy | Vampire |
| Lixin | Model Elimination withou Contrapositives and its Application to PTTP | SPASS |
| Rogelio | Equality and Paramodulation | Bliksem |
| Date (papers) | Time | Place | Speakers |
|---|---|---|---|
| Thu, May 2 | 2:30-3:45pm | 113 MLH |
Haiou Lixin |
| Fri, May 3 | 3:30-5:00pm | 205 MLH |
Ben Chris George |
| Tue, May 7 | 2:40-3:45pm | 113 MLH |
Joiey Rogelio |
| Date (systems) | Time | Place | Speakers |
| Thu, May 16 | 2:15-4:15pm | 113MLH |
Ben Chris George Joiey |
| Fri, May 17 | 1:00-2:15pm | B11 MLH |
Haiou Lixin Rogelio |