|
||||||||
|
||||||||
| Invited Talk | |
| 09:00 - 10:00 | Catherine Meadows: A Cryptographer's Garden of Equational Theories: Interesting Unification Problems from Cryptography |
| Regular papers UNIF/ADDCT | |
| 10:30 - 11:00 | UNIF: Michael Franssen: Implementing Rigid E-Unification |
| 11:00 - 11:30 | UNIF: Sunil Kothari, James Caldwell: A Machine Checked Model of MGU Axioms: Applications of Finite Maps and Functional Induction |
| 11:30 - 12:00 | UNIF: Temur Kutsia, Mircea Marin: Order-Sorted Unification with Regular Expression Sorts |
| 12:00 - 12:30 | ADDCT: Sergey Babenyshev, Vladimir Rybakov, Renate A. Schmidt, Dmitry Tishkovsky: A Tableau Method for Checking Rule Admissibility in S4 |
| Work in progress/Presentation only papers (ADDCT) | |
| 14:00 - 14:30 | ADDCT: Grant Olney Passmore, Leonardo de Moura: Universality of Polynomial Positivity and a Variant of Hilbert's 17th Problem |
| 14:30 - 14:55 | ADDCT: Renate A. Schmidt: The Ackermann Approach for Modal Logic, Correspondence Theory and Second-Order Reduction |
| 14:55 - 15:20 | ADDCT: Lan Zhang, Ullrich Hustadt, Clare Dixon: CTL-RP: A Computational Tree Logic Resolution Prover |
| Work in progress/Presentation only papers (UNIF) | |
| 16:00-16:25 | UNIF: Pascal Fontaine: Combinations of theories for decidable fragments of first-order logic |
| 16:25-16:50 | UNIF: Franz Baader and Barbara Morawska: Unification in the Description Logic EL |
| 16:50-17:15 | UNIF: Enrica Nicolini, Christophe Ringeissen and Michael Rusinowitch: Decision Procedures for Data Structures Combined with Shared Fragments of Arithmetic |
| 17:15-17:40 | UNIF: Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran and Michael Rusinowitch: Cap Unification: Application to Protocol Security modulo Homomorphic Encryption |
| Business | |
| 17:45 - 18:00 | UNIF Business meeting |
