| CERES in Many-Valued Logics / Matthias Baaz ; Alexander Leitsch |
| A Decomposition Rule for Decision Procedures by Resolution-Based Calculi / Ullrich Hustadt ; Boris Motik ; Ulrike Sattler |
| Abstract DPLL and Abstract DPLL Modulo Theories / Robert Nieuwenhuis ; Albert Oliveras ; Cesare Tinelli |
| Combining Lists with Non-stably Infinite Theories / Pascal Fontaine ; Silvio Ranise ; Calogero G. Zarba |
| Abstract Model Generation for Preprocessing Clause Sets / Miyuki Koshimura ; Mayumi Umeda ; Ryuzo Hasegawa |
| Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying / Helmut Seidl ; Kumar Neeraj Verma |
| Applications of General Exact Satisfiability in Propositional Logic Modelling / Vilhelm Dahllof |
| BCiC: A System for Code Authenticationand Verification / Nathan Whitehead ; Mart'in Abadi |
| Ordered Resolution with Selection for H(@) / Carlos Areces ; Daniel Gor'in |
| On a Semantic Subsumption Test / Jerzy Marcinkowski ; Jan Otop ; Grzegorz Stelmaszek |
| Suitable Graphs for Answer Set Programming / Thomas Linke ; Vladimir Sarsakov |
| Weighted Answer Sets and Applications in Intelligence Analysis / Davy Van Nieuwenborgh ; Stijn Heymans ; Dirk Vermeir |
| How to Fix It: Using Fixpoints in Different Contexts / Igor Walukiewicz |
| Reasoning About Systems with Transition Fairness / Benjamin Aminof ; Thomas Ball ; Orna Kupferman |
| Entanglement - A Measure for the Complexity of Directed Graphs with Applications to Logic and Games / Dietmar Berwanger ; Erich Gradel |
| How the Location of * Influences Complexity in Kleene Algebra with Tests / Chris Hardin |
| The Equational Theory of Is Decidable, but Not Finitely Axiomatisable / Roberto Di Cosmo ; Thomas Dufour |
| A Trichotomy in the Complexity of Propositional Circumscription / Gustav Nordh |
| Exploiting Fixable, Removable, and Implied Values in Constraint Satisfaction Problems / Lucas Bordeaux ; Marco Cadoli ; Toni Mancini |
| Evaluating QBFs via Symbolic Skolemization / Marco Benedetti |
| The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs / Jürgen Giesl ; Rene Thiemann ; Peter Schneider-Kamp |
| Automated Termination Analysis for Incompletely Defined Programs / Christoph Walther ; Stephan Schweitzer |
| Automatic Certification of Heap Consumption / Lennart Beringer ; Martin Hofmann ; Alberto Momigliano ; Olha Shkaravska |
| A Formalization of Off-Line Guessing for Security Protocol Analysis / Paul Hankes Drielsma ; Sebastian Mödersheim ; Luca Vigano |
| Abstraction-Carrying Code / Elvira Albert ; German Puebla ; Manuel Hermenegildo |
| A Verification Environment for Sequential Imperative Programs in Isabelle/HOL / Norbert Schirmer |
| Can a Higher-Order and a First-Order Theorem Prover Cooperate? / Christoph Benzmüller ; Volker Sorge ; Mateja Jamnik ; Manfred Kerber |
| A Generic Framework for Interprocedural Analyses of Numerical Properties / Markus Müller-Olm |
| Second-Order Matching via Explicit Substitutions / Flávio L.C. de Moura ; Fairouz Kamareddine ; and |
| Mauricio Ayala-Rincon |
| Knowledge-Based Synthesis of Distributed Systems Using Event Structures / Mark Bickford ; Robert C. Constable ; Joseph Y. Halpern ; Sabina Petride |
| The Inverse Method for the Logic of Bunched Implications / Kevin Donnelly ; Tyler Gibson ; Neel Krishnaswami ; Stephen Magill ; Sungwoo Park |
| Cut-Elimination: Experiments with CERES / Stefan Hetzl ; Clemens Richter ; Hendrik Spohr |
| Uniform Rules and Dialogue Games for Fuzzy Logics / Agata Ciabattoni ; Christian G. Fermüller ; George Metcalfe |
| Nonmonotonic Description Logic Programs: Implementation and Experiments / Thomas Eiter ; Giovambattista Ianni ; Roman Schindlauer ; Hans Tompits |
| Implementing Efficient Resource Management for Linear Logic Programming / Pablo López ; Jeff Polakow |
| Layered Clausal Resolution in the Multi-modal Logic of Beliefs and Goals / Jamshid Bagherzadeh ; S. Arun-Kumar |
| Author Index |
| CERES in Many-Valued Logics / Matthias Baaz ; Alexander Leitsch |
| A Decomposition Rule for Decision Procedures by Resolution-Based Calculi / Ullrich Hustadt ; Boris Motik ; Ulrike Sattler |
| Abstract DPLL and Abstract DPLL Modulo Theories / Robert Nieuwenhuis ; Albert Oliveras ; Cesare Tinelli |
| Combining Lists with Non-stably Infinite Theories / Pascal Fontaine ; Silvio Ranise ; Calogero G. Zarba |
| Abstract Model Generation for Preprocessing Clause Sets / Miyuki Koshimura ; Mayumi Umeda ; Ryuzo Hasegawa |
| Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying / Helmut Seidl ; Kumar Neeraj Verma |
