Session 1 | ||
14.30 - 15.30 | Daniel Leivant | Intrinsic theories: a
methodology for reasoning about functional programs and their computational complexity |
15.30 - 16.00 | Alan Bundy, Julian Richardson |
Proofs About Lists Using Ellipsis |
Coffee break | ||
Session 2 | ||
16.30 - 17.00 | Miki Hermann, Laurent Juban, Phokion G. Kolaitis |
On the Complexity of Counting the Hilbert Basis of a Linear Diophantine System |
17.00 - 17.30 | Ramon Bejar Felip Manya |
Solving Combinatorial Problems with Regular Local Search Algorithms |
17.30 - 18.00 | Anatoli Degtyarev, Alexander Lyaletski Marina Morokhovets |
Evidence Algorithm and sequent-style logical inference search |
Welcoming dinner (19:00) |
Georgian Session 1 | ||
10.00 - 10.30 | ||
10.30 - 11.00 | ||
Coffee break | ||
Georgian Session 2 | ||
11.30 - 12.00 | ||
12.00 - 12.30 | ||
Lunch | ||
Session 3 | ||
14.30 - 15.00 | Serenella Cerrito, Marta Cialdea Mayer, Sebastien Praud |
First Order Linear Temporal Logic over Finite Time Structures |
15.00 - 15.30 | Martin Leucker | Model Checking Games for the Alternation-Free mu-Calculus and Alternating Automata |
15.30 - 16.00 | Stephan Merz, Yassine Mokhtari |
Efficiently executable TLA |
Session 4 | ||
16.30 - 17.00 | Enno Ohlebusch | Transforming Conditional Rewrite Systems with Extra Variables into Unconditional Systems |
17.00 - 17.30 | Uwe Waldmann | Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups |
17.30 - 18.00 | Pierre Rety | Regular Sets of Descendants for Constructor-based Rewrite Systems |
Full-day excursion (10:00) |
Poster Session | ||
10.00 - 11.00 | Wojciech Penczek, Rob Gerth, Ruurd Kuiper Domenico Cantone, Alberto G. Zarba, Andrea Formisano, Eugenio G. Omodeo, Emmanouil Marakakis |
Partial Order Reductions Preserving Simulations Folding Quantifiers into Map Composition Correctness of Logic Programs Constructed by a Schema-Based Methods |
Coffee break | ||
Session 5 | ||
11.30 - 12.00 | Ian Horrock, Ulrike Sattler, Stephan Tobies |
Practical Reasoning for Expressive Description Logics |
12.00 - 12.30 | Carsten Lutz | Complexity of Terminological Reasoning Revisited |
Lunch | ||
Session 6 | ||
14.30 - 15.30 | Yuri Gurevich | Invited talk |
15.30 - 16.00 | Georg Gottlob, Christos Papadimitriou |
On the Complexity of Single-Rule Datalog Queries |
Coffee break | ||
Session 7 | ||
16.30 - 17.00 | Rene Moreno | Abstracting Properties in Concurrent Constraint Programming |
17.00 - 17.30 | Roberta Gori | A fixpoint semantics for reasoning about finite failure |
17.30 - 18.00 | Jeremy Gow, Alan Bundy, Ian Green |
Extensions to the Estimation Calculus |
Session 8 | ||
10.00 - 10.30 | Eva Hoogland, Maarten Marx, Martin Otto |
Beth definability for the guarded fragment |
10.30 - 11.00 | Michael Dierkes | Simplification of Horn Clauses that are Clausal Forms of Guarded Formulas |
Coffee break | ||
Session 9 | ||
11.30 - 12.00 | Pablo Lopez, Ernesto Pimentel |
Resource Management in Linear Logic Proof Search Revisited |
12.00 - 12.30 | Jean-Marc Andreoli, Roberto Maieli |
Focusing and Proof-Nets in Linear and Non-Commutative Logic |
Lunch | ||
Session 10 | ||
14.30 - 15.00 | Bart Demoen, Konstantinos Sagonas |
CHAT is $\Theta$(SLG-WAM) |
15.00 - 15.30 | Nikolay Pelov, Maurice Bruynooghe |
Proving Failure of Queries for Definite Logic Programs Using XSB-Prolog |
15.30 - 16.00 | Elvira Albert, Maria Alpuente, Michael Hanus, German Vidal |
A Partial Evaluation Framework for Curry Programs |
Coffee break | ||
Session 11 | ||
16.30 - 17.30 | Matthias Baaz | Term Induction and Herbrand's Theorem |
Farewell dinner (19:00) |
Only for those who registered for both LPAR and LLC.
Travel by bus to Zestafoni and Batumi (10:00) |
Talks by Georgian logicians. Abstracts will be added here.
Dinner at the Svanetian restaurant "Ushba". Svanetia is part of Georgia situated in high mountains. The dinner will feature a variety of meals (over 10) and of course the Georgian atmosphere.
Dinner at the fish restaurant "Over Kura". Kura is the river flowing through Tbilisi. As the name suggests, the restaurant is built in a way that it "hangs" over the river.