| Marco Benedetti. Evaluating QBFs via Symbolic Skolemization |
| Ullrich Hustadt, Boris Motik and Ulrike Sattler. A Decomposition Rule for Decision Procedures by Resolution-based Calculi |
| Carsten Schuermann and Mark-Oliver Stehr. An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf |
| Nathan Whitehead and Martín Abadi. BCiC: A System for Code Authentication and Verification |
| Mark Bickford, Robert Constable, Joseph Halpern and Sabina Petride. Knowledge-Based Synthesis of Distributed Systems Using Event Structures |
| Christoph Walther and Stephan Schweitzer. Automated Termination Analysis for Incompletely Defined Programs |
| Christopher Hardin. How the Location of * Influences Complexity in Kleene Algebra with Tests |
| Thomas Linke and Vladimir Sarsakov. Suitable Graphs for Answer Set Programming |
| Pascal Fontaine, Silvio Ranise and Calogero G. Zarba. Combining Lists with Non-Stably Infinite Theories |
| Thomas Eiter, Giovambattista Ianni, Roman Schindlauer and Hans Tompits. Nonmonotonic Description Logic Programs: Implementation & Experiments |
| Lennart Beringer, Martin Hofmann, Alberto Momigliano and Olha Shkaravska. Automatic Certification of Heap Consumption |
| George Metcalfe, Agata Ciabattoni and Christian Fermueller. Uniform Rules and Dialogue Games for Fuzzy Logics |
| Jerzy Marcinkowski, Jan Otop and Grzegorz Stelmaszek. On a Semantic Subsumption Test |
| Miyuki Koshimura, Mayumi Umeda and Ryuzo Hasegawa. Abstract Model Generation for Preprocessing Clause Sets |
| Albert Oliveras, Robert Nieuwenhuis and Cesare Tinelli. Abstract DPLL and Abstract DPLL Modulo Theories |
| Vilhelm Dahllof. Applications of General Exact Satisfiability in Propositional Logic Modelling |
| Roberto Di Cosmo and Thomas Dufour. The theory of <N,0,1,+,.,^> is decidable, but not finitely axiomatisable. |
| Dietmar Berwanger and Erich Graedel. Entanglement -- A Measure for the Complexity of Directed Graphs With Applications to Logic and Games |
| Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Stephen Magill and Sungwoo Park. The Inverse Method for the Logic of Bunched Implications |
| Jeff Polakow and Pablo Lopez. Implementing Efficient Resource Management for Linear Logic Programming |
| Daniel Gorín and Carlos Areces. Ordered resolution with selection for H(@) |
| Paul Hankes Drielsma, Sebastian Mödersheim and Luca Viganň. A Formalization of Off-Line Guessing for Security Protocol Analysis |
| Davy Van Nieuwenborgh, Stijn Heymans and Dirk Vermeir. Weighted Answer Sets and Applications in Intelligence Analysis |
| Norbert Schirmer. A Verification Environment for Sequential Imperative Programs in Isabelle/HOL |
| Bejamin Aminof, Thomas Ball and Orna Kupferman. Reasoning about Systems with Transition Fairness |
| Helmut Seidl and Kumar Neeraj Verma. Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying |
| Flavio L. C. de Moura, Fairouz Kamareddine and Mauricio Ayala Rincon. Second-Order Matching via Explicit Substitutions |
| Jamshid Bagherzadeh and S. Arun-Kumar . Layered Clausal Resolution in the Multi-Modal Logic of Beliefs and Goals |
| Stefan Hetzl, Matthias Baaz, Alexander Leitsch, Clemens Richter and Hendrik Spohr. Cut-Elimination: Experiments with CERES |
| Lucas Bordeaux, Marco Cadoli and Toni Mancini. Exploiting Fixable, Substitutable and Determined Values in Constraint Satisfaction Problems |
| German Puebla, Manuel Hermenegildo and Elvira Albert. Abstraction-Carrying Code |
| Christoph Benzmueller, Volker Sorge, Mateja Jamnik and Manfred Kerber. Can a Higher-Order and a First-Order Theorem Prover Cooperate? |
| Gustav Nordh. A Trichotomy in the Complexity of Propositional Circumscription |