Bringing Computer Science
Logic to all parts
of the world


Preliminary programme


LPAR-07 Program

Monday, October 15th

12:30-14:05 Workshop. Session 1.
12:30Norbert Preining
 Kripke Frames, Gödel Logics, and beyond (invited talk)
13:15Helmut Veith
 On the Secrecy of Proofs
13:40Matthias Baaz
 Decidability and undecidability of the extendability of partial proof descriptions

14:05-14:30 Coffee Break, Registration Starts

14:30-16:05 Workshop. Session 2.
14:30Richard Zach
 Analytic systems for the epsilon calculus (invited talk)
15:15Chris Fermüller
 Interpreting interval based fuzzy logics
15:40Michel Parigot
 On the formalization of constructivity
16:15-18:15 Session: Non-Classical Logics. Short papers.
16:15Opening
16:30Matthias Baaz, Agata Ciabattoni, Christian Fermueller
 Monadic Fragments of Gödel Logics: Decidability and Undecidability Results
17:00Luigi Santocanale, Yde Venema
 Completeness for flat modal fixpoint logics
17:30Marc Bezem, Tore Langholm, Michal Walicki
 Completeness and Decidability in Sequence Logic
18:00Laura Kovacs. Aligator: a Package for Reasoning about Loops

20:00 Reception (Hotel Bass)

Tuesday, October 16th

09:00-10:30 Session: Invited Talk
09:00 Richard Waldinger (SRI International)
  Whatever Happened to Deductive Question Answering? (invited talk)
10:00Michel Ludwig, Uwe Waldmann
 An Extension of the Knuth-Bendix Ordering with LPO-like Properties

10:30-10:55 Coffee Break

10:55-12:55 Session: Protocol Verification
10:55Francien Dechesne, Mohammadreza Mousavi, Simona Orzan
 Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap
11:25Veronique Cortier, Stephanie Delaune
 Deciding knowledge in security protocols for monoidal equational theories
11:55Yannick Chevalier, Denis Lugiez, Michael Rusinowitch
 Verifying Cryptographic Protocols with Subterm Constraints
12:25Stéphanie Delaune, Hai Lin, Christopher Lynch
 Protocol verification via rigid/flexible resolution

12:55-14:05 Lunch

14:05-16:05 Session: Rewriting. Short Papers
14:05Marko Samer, Stefan Szeider
 Algorithms for Propositional Model Counting
14:35Frederic Blanqui, Jean-Pierre Jouannaud, Albert Rubio
 HORPO with Computability Closure : A Reconstruction
15:05Philippe de Groote, Sarah Maarek, Ryo Yoshinaka
 On two Extensions of Abstract Categorial Grammars
15:35Alexis Saurin. Typing streams in the $\Lambda\mu$-calculus: extended abstract

16:05-16:30 Coffee Break

16:30-19:00 Session: Theorem Proving
16:30Behzad Akbarpour, Lawrence Paulson
 Extending Resolution to Prove Inequalities On Elementary Functions
17:00Richard Bonichon, David Delahaye, Damien Doligez
 Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs
17:30Josef Urban, Geoff Sutcliffe
 ATP cross-verification of the Mizar MPTP Challenge problems
18:00Eric Jaeger, catherine dubois
 Why would you trust B?

Wednesday, October 17th

10:00-18:30 Excursion

The participants will be picked up at 10:00 at their hotels.

20:00-23:00 Conference Dinner

Thursday, October 18th

09:00-10:30 Session: Invited Talk

10:30-10:55 Coffee Break

09:00 Janos Makowsky (Technion - Israel Institute of Technology)
  From Hilbert's Program to a Logic Toolbox (invited talk)
10:00Emanuel Kieronski, Lidia Tendera
 On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Relations
10:55-12:55 Session: Temporal Logic and Model Checking
10:55Roland Axelsson, Martin Lange
 Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic
11:25Pietro Abate, Rajeev Gore, Florian Widmann
 One-pass Tableaux for Computation Tree Logic
11:55Demri Stéphane, Alexander Rabinovich
 The complexity of temporal logic with until and since over ordinals
12:25Aniello Murano, Alessandro Ferrante, Mimmo Parente
 Enriched $\mu$--Calculus Pushdown Module Checking

12:55-14:15 Lunch

14:15-16:15 Session: Description Logics
14:15Evgeny Zolin, Yevgeny Kazakov, Ulrike Sattler
 How Many Legs Do I Have? Non-Simple Roles in Number Restrictions Revisited
14:45Adila Krisnadhi, Carsten Lutz
 Data Complexity in the EL family of Description Logics
15:15Maja Milicic
 Complexity of Planning in Action Formalisms based on Description Logics
15:45Timo Weithoener. U2R2 - The Ulm University Relational Reasoner: System Description
16:00Claudia Obermaier and Ulrich Furbach. Knowledge Compilation for Description Logics

16:15-16:45 Coffee Break

16:45-17:15 Session: Description Logics and Non-Monotonic Reasoning
16:30Sebastian Brandt
 Matching in hybrid terminologies
17:00Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato
 Preferential Description Logics

Friday, October 19th

09:00-10:30 Session: Invited Talk
09:00 Helmut Veith (Technische Universität München)
  On the Notion of Vacuous Truth (invited talk)
10:00Aharon Abadi, Alexander Rabinovich, Mooly Sagiv
 Decidable Fragments of Many-Sorted Logic

10:30-10:55 Coffee Break

10:55-12:55 Session: Linear Logic
10:55David Baelde, Dale Miller
 Least and greatest fixed points in linear logic
11:25Gabriele Pulcini
 Permutative Additives and Exponentials
11:55Damiano Mazza, Michele Pagani
 The Separation Theorem for Differential Interaction Nets
12:25Roberto Maieli
 Retractile proof-nets of the purely multiplicative and additive fragment of Linear Logic

12:55-14:15 Lunch

14:15-16:45 Session: Non-Monotonic Reasoning
14:15Luís Moniz Pereira, Alexandre Miguel Pinto
 Approved Models for Normal Logic Programs
14:45Mantas Simkus, Thomas Eiter
 FDNC: Decidable Non-monotonic Disjunctive Logic Programs with Function Symbols
15:15Leopoldo Bertossi, Loreto Bravo
 The Semantics of Consistency and Trust in Peer Data Exchange Systems

15:45-16:15 Coffee Break

16:15-18:00 Last Session
16:15Maarten Mariën, Johan Wittocx, Marc Denecker
 Integrating inductive definitions in SAT
16:45Zaynah Dargaye, Xavier Leroy
 Mechanized verification of CPS transformations
17:15Sona Aleksanyan and Anahit Chubaryan. On determinative complexity of Frege proofs
17:30Ozan Kahramanogullari. On Linear Logic Planning and Concurrency
17:45Luís Moniz Pereira and Ari Saptawijaya. Moral Decision Making with ACORDA

20:00-24:00 Farewell Dinner (restaurant Parvana)

Note that we will be sitting outdoors, so dress appropriately.