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