LPAR 2004
Logic for Programming, Aritificial Intelligence and Reasoning

Montevideo
March 13-18, 2005

Sunday, March 13

Workshops

The Workshop programmes will be available on the workshop Web pages.

Monday, March 14

Session 1
 09:00-10:00   Alexander Leitsch  CERES: Cut-Elimination by Resolution (invited talk)
 10:00-10:30    Coffee break
Session 2
 10:30-11:00   Ullrich Hustadt,
 Boris Motik,
 Ulrike Sattler		  A Decomposition Rule for Decision Procedures by
 Resolution-based Calculi
 11:00-11:30   Albert Oliveras,
 Robert Nieuwenhuis,
 Cesare Tinelli		  Abstract DPLL and Abstract DPLL Modulo Theories
 11:30-12:00   Pascal Fontaine,
 Silvio Ranise,
 Calogero G. Zarba		  Combining Lists with Non-Stably Infinite Theories
 12:00-12:30   Miyuki Koshimura,
 Mayumi Umeda,
 Ryuzo Hasegawa		  Abstract Model Generation for Preprocessing Clause Sets
 12:30-14:00    Lunch
Session 3
 14:00-14:30   Helmut Seidl,
 Kumar Neeraj Verma		  Flat and One-Variable Clauses: Complexity of
 Verifying Cryptographic Protocols
 with Single Blind Copying
 14:30-15:00   Vilhelm Dahllof  Applications of General Exact Satisfiability in
 Propositional Logic Modelling
 15:00-15:30   Nathan Whitehead,
 Martín Abadi		  BCiC: A System for Code Authentication and Verification
 15:30-16:00    Coffee break
Session 4
 16:00-16:30   Daniel Gorín,
 Carlos Areces		  Ordered resolution with selection for H(@)
 16:30-17:00   Jerzy Marcinkowski,
 Jan Otop,
 Grzegorz Stelmaszek		  On a Semantic Subsumption Test
 17:00-17:30   Thomas Linke,
 Vladimir Sarsakov		  Suitable Graphs for Answer Set Programming
 17:30-18:00   Davy Van Nieuwenborgh,
 Stijn Heymans,
 Dirk Vermeir		  Weighted Answer Sets and Applications in
 Intelligence Analysis
  19:00 Welcoming dinner

Tuesday, March 15

tutorials.cgi#abadi
Session 1
 09:00-10:00   Igor Walukiewicz  How to fix it: using fixpoints in different
 contexts (invited talk)
 10:00-10:30    Coffee break
Session 2
 10:30-11:00   Bejamin Aminof,
 Thomas Ball,
 Orna Kupferman		  Reasoning about Systems with Transition Fairness
 11:00-11:30   Dietmar Berwanger,
 Erich Graedel		  Entanglement -- A Measure for the Complexity of
 Directed Graphs With Applications to
 Logic and Games
 11:30-12:00   Christopher Hardin  How the Location of * Influences Complexity in
 Kleene Algebra with Tests
 12:00-12:30   Roberto Di Cosmo,
 Thomas Dufour		  The theory of <N,0,1,+,.,^> is decidable
 but not finitely axiomatisable
 12:30-14:00    Lunch
Session 3
 14:00-14:30   Gustav Nordh  A Trichotomy in the Complexity of
 Propositional Circumscription
 14:30-15:00   Lucas Bordeaux,
 Marco Cadoli,
 Toni Mancini		  Exploiting Fixable, Substitutable and Determined
 Values in Constraint Satisfaction Problems
 15:00-15:30   Marco Benedetti  Evaluating QBFs via Symbolic Skolemization
 15:30-16:00    Coffee break
Session 4
 16:00-18:00   Martin Abadi  Reasoning about Security Protocols (tutorial)

Wednesday, March 18

  10:00-18:00 Excursion

Thursday, March 17

Session 1
 09:00-10:00   Jürgen Giesl  The Dependency Pair Framework:
 Combining Techniques for Automated
 Termination Proofs (invited talk)
 10:00-10:30    Coffee break
Session 2
 10:30-11:00   Christoph Walther,
 Stephan Schweitzer		  Automated Termination Analysis for
 Incompletely Defined Programs
 11:00-11:30   Lennart Beringer,
 Martin Hofmann,
 Alberto Momigliano,
 Olha Shkaravska		  Automatic Certification of Heap Consumption
 11:30-12:00   Paul Hankes Drielsma,
 Sebastian Mödersheim,
 Luca Viganň		  A Formalization of Off-Line Guessing for
 Security Protocol Analysis
 12:00-12:30   German Puebla,
 Manuel Hermenegildo,
 Elvira Albert		  Abstraction-Carrying Code
 12:30-14:00    Lunch
Session 3
 14:00-14:30   Norbert Schirmer  A Verification Environment for Sequential
 Imperative Programs in Isabelle/HOL
 14:30-15:00   Carsten Schuermann,
 Mark-Oliver Stehr		  An Executable Formalization of the HOL/Nuprl
 Connection in the Metalogical Framework Twelf
 15:00-15:30   Christoph Benzmueller,
 Volker Sorge,
 Mateja Jamnik,
 Manfred Kerber		  Can a Higher-Order and a First-Order
 Theorem Prover Cooperate?
 15:30-16:00    Coffee break
Session 4
 16:00-18:00   Ian Horrocks  Description Logic Reasoning
  19:00 Conference dinner

Friday, March 18

Session 1
 09:00-10:00   Helmut Seidel  TBA (invited talk)
 10:00-10:30    Coffee break
Session 2
 10:30-11:00   Flavio L. C. de Moura,
 Fairouz Kamareddine,
 Mauricio Ayala Rincon		  Second-Order Matching via Explicit Substitutions
 11:00-11:30   Mark Bickford,
 Robert Constable,
 Joseph Halpern,
 Sabina Petride		  Knowledge-Based Synthesis of Distributed Systems
 Using Event Structures
 11:30-12:00   Kevin Donnelly,
 Tyler Gibson,
 Neel Krishnaswami,
 Stephen Magill,
 Sungwoo Park		  The Inverse Method for the Logic of Bunched Implications
 12:00-12:30   Stefan Hetzl,
 Matthias Baaz,
 Alexander Leitsch,
 Clemens Richter,
 Hendrik Spohr		  Cut-Elimination: Experiments with CERES
 12:30-14:00    Lunch
Session 3
 14:00-14:30   George Metcalfe,
 Agata Ciabattoni,
 Christian Fermueller		  Uniform Rules and Dialogue Games for Fuzzy Logics
 14:30-15:00   Jamshid Bagherzadeh,
 S. Arun-Kumar		  Layered Clausal Resolution in the Multi-Modal
 Logic of Beliefs and Goals
 15:00-15:30   Thomas Eiter,
 Giovambattista Ianni,
 Roman Schindlauer,
 Hans Tompits		  Nonmonotonic Description Logic Programs:
 Implementation & Experiments
 15:30-16:00   Jeff Polakow,
 Pablo Lopez		  Implementing Efficient Resource Management
 for Linear Logic Programming