| Authors | Title | Paper | Talk |
|---|
| Guy Avni, Orna Kupferman and Tami Tamir | From Reachability to Temporal Specifications in Cost-Sharing Games |  | |
| Veronique Cortier | Electronic voting: how logic can help | | |
| Rajeev Gore | And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL | | Jul 19 10:45 |
| Kenneth McMillan | Structured Search and Learning | | Jul 22 10:45 |
| Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel | Unified Classical Logic Completeness: A Coinductive Pearl | | Jul 19 11:45 |
| Fredrik Lindblad | A Focused Sequent Calculus for Higher-Order Logic | | Jul 19 12:15 |
| Ori Lahav and Yoni Zohar | SAT-based Decision Procedure for Analytic Pure Sequent Calculi | | Jul 19 14:30 |
| Marijn Heule, Martina Seidl and Armin Biere | Unified Proof System for QBF Preprocessing | | Jul 19 15:00 |
| Carlos Ansótegui, Maria Luisa Bonet, Jesus Giráldez-Cru and Jordi Levy | The Fractal Dimension of SAT Formulas | | Jul 19 15:30 |
| Paula Chocron, Pascal Fontaine and Christophe Ringeissen | A Gentle Non-Disjoint Combination of Satisfiability Procedures | | Jul 19 16:30 |
| Sophie Tourret, Mnacho Echenim and Nicolas Peltier | A Rewriting Strategy to Generate Prime Implicates in Equational Logic | | Jul 20 10:45 |
| Peter Baumgartner, Joshua Bax and Uwe Waldmann | Finite Quantification in Hierarchic Theorem Proving | | Jul 20 11:15 |
| Josh Berdine and Nikolaj Bjorner | Computing All Implied Equalities via SMT-based Partition Refinement | | Jul 20 11:45 |
| Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Stroeder, Steffi Swiderski and Rene Thiemann | Proving Termination of Programs Automatically with AProVE | | Jul 20 12:15 |
| Matthias Horbach and Viorica Sofronie-Stokkermans | Locality Transfer: From Constrained Axiomatizations to Reachability Predicates | | Jul 20 14:30 |
| Thomas Stroeder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel and Peter Schneider-Kamp | Proving Termination and Memory Safety for Programs with Pointer Arithmetic | | Jul 20 15:00 |
| Wenhui Zhang | QBF Encoding of Temporal Properties and QBF-Based Verification | | Jul 20 15:30 |
| Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai and Daniel Weller | Introducing quantified cuts in logic with equality | | Jul 20 16:30 |
| Vivek Nigam, Giselle Reis and Leonardo Lima | Quati: An Automated Tool for Proving Permutation Lemmas | | Jul 20 17:00 |
| Rajeev Gore, Jimmy Thomson and Jesse Wu | A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description | | Jul 20 17:20 |
| Jens Otten | MleanCoP: A Connection Prover for First-Order Modal Logic | | Jul 20 17:40 |
| Serenella Cerrito, Amélie David and Valentin Goranko | Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+ | | Jul 21 10:45 |
| Jean-Baptiste Jeannin and André Platzer | dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems | | Jul 21 11:15 |
| Bjoern Lellmann | Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications | | Jul 21 11:45 |
| Cláudia Nalon, João Marcos and Clare Dixon | Clausal Resolution for Modal Logics of Confluence | | Jul 21 12:15 |
| Rajeev Gore, Kerry Olesen and Jimmy Thomson | Implementing Tableaux Calculi Using BDDs: BDDTab System Description | | Jul 21 12:45 |
| Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Ruemmer | Approximations for Model Construction | | Jul 21 14:30 |
| Rüdiger Ehlers and Martin Lange | A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic | | Jul 21 15:00 |
| Aaron Stump, Geoff Sutcliffe and Cesare Tinelli | StarExec: a Cross-Community Infrastructure for Logic Solving | | Jul 21 15:20 |
| Bruno Woltzenlogel Paleo, Joseph Boudou and Andreas Fellner | Skeptik [System Description] | | Jul 21 15:40 |
| Fabio Papacchini and Renate A. Schmidt | Terminating Minimal Model Generation Procedures for Propositional Modal Logics | | Jul 21 16:00 |
| Daniel Gorin, Dirk Pattinson, Lutz Schröder, Thorsten Wißmann and Florian Widmann | COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) | | Jul 21 16:30 |
| Olaf Beyersdorff and Leroy Chew | The Complexity of Theorem Proving in Circumscription and Minimal Entailment | | Jul 22 11:45 |
| Laura Bozzelli and Cesar Sanchez | Visibly Linear Temporal Logic | | Jul 22 12:15 |
| Patrick Koopmann and Renate A. Schmidt | Count and Forget: Uniform Interpolation of SHQ-Ontologies | | Jul 22 14:30 |
| Andreas Steigmiller, Birte Glimm and Thorsten Liebig | Coupling Tableau Algorithms for Expressive Description Logics with Completion-based Saturation Procedures | | Jul 22 15:00 |
| David Carral, Cristina Feier, Bernardo Cuenca Grau, Pascal Hitzler and Ian Horrocks | EL-ifying Ontologies | | Jul 22 15:30 |
| İsmail İlkan Ceylan and Rafael Peñaloza | The Bayesian Description Logic BEL | | Jul 22 16:30 |
| Michael Beeson and Larry Wos | Otter proofs in Tarskian geometry | | Jul 22 17:00 |
| Nicola Olivetti and Gian Luca Pozzato | NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics | | Jul 22 17:30 |
| Adam Pease and Stephan Schulz | Knowledge Engineering for Large Ontologies with Sigma KEE 3.0 | | Jul 22 17:50 |