Regular papers

Wolfgang Ahrendt, Chalmers U of Techn., Sweden
Deductive search for errors in free data type specifications using model generation

Jean-Marc Andreoli, Xerox Grenoble, France
Focussing proof-net construction as a middleware paradigm

Gilles Audemard, ITC-irst, Italy and Belaid Benhamou, LSIS Marseille, France
Reasoning by symmetry and function ordering in finite model generation

Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, and Roberto Sebastiani; ITC-irst, Italy
A SAT based approach for solving formulas over boolean and linear mathematical propositions

Andrew Bernard and Peter Lee, Carnegie Mellon U, USA
Temporal logic for proof-carrying code

Miquel Bofill, U Girona, Spain and Albert Rubio, Techn. U of Catalonia, Spain
Well-foundedness is sufficient for completeness of ordered paramodulation

Cristina Borralleras, U Vic, Spain; Salvador Lucas, Polytechnic U of Valencia, Spain; and Albert Rubio, Techn. U of Catalonia, Spain
Recursive path orderings can be context-sensitive

Chad E. Brown, Carnegie Mellon U, USA
Solving for set variables in higher-order theorem proving

Thierry Boy de la Tour, IMAG Grenoble, France
A note on symmetry heuristics in SEM

Leonardo de Moura, Harald Rueß, and Maria Sorea; SRI International, USA
Lazy theorem proving for bounded model checking over infinite domains

Uwe Egly, Vienna U of Techn., Austria
Embedding lax logic into intuitionistic logic

Jonathan Ford, U New England, Australia and Natarajan Shankar, SRI International, USA
Formal verification of a combination decision procedure

Didier Galmiche and Daniel Mery, LORIA Nancy, France
Connection-based proof search in propositional BI logic

Harald Ganzinger, MPI Saarbrücken, Germany
Shostak light

Lilia Georgieva, U Manchester, UK; Ullrich Hustadt, U Liverpool, UK; and Renate A. Schmidt, U Manchester, UK
A new clausal class decidable by hyperresolution

Eugene Goldberg, Cadence Design Systems, USA
Testing satisfiability of CNF formulas by computing a stable set of points

Bernhard Gramlich and Reinhard Pichler, Vienna U of Techn., Austria
Algorithmic aspects of herbrand models represented by ground atoms with ground equations

Thomas Hillenbrand, MPI Saarbrücken, Germany and Bernd Löchner, U Kaiserslautern, Germany
The next Waldmeister loop

Orna Kupferman, Hebrew U of Jerusalem, Israel; Ulrike Sattler, Dresden U of Techn., Germany; and Moshe Y. Vardi, Rice U, USA
The complexity of the graded µ-calculus

Dominique Larchey-Wendling, LORIA Nancy, France
Combining proof-search and counter-model construction for deciding Gödel-Dummett logic

Christopher Lynch and Barbara Morawska, Clarkson U, USA
Basic syntactic mutation

George C. Necula and Robert R. Schneck, U California-Berkeley, USA
A gradual approach to a more trustworthy, yet scalable, proof-carrying code

Guoqiang Pan, Rice U, USA; Ulrike Sattler, Dresden U of Techn., Germany; and Moshe Y. Vardi, Rice U, USA
BDD-based decision procedures for K

Lawrence C. Paulson, U Cambridge, UK
The reflection theorem: A study in formalizing meta-theoretic reasoning

Martin Strecker, Techn. U of Munich, Germany
Formal verification of a java compiler in isabelle

Aaron Stump and David L. Dill, Stanford U, USA
Faster proof checking in the Edinburgh Logical Framework

Calogero G. Zarba, Stanford U, USA
Combining multisets with integers

System descriptions

Carlos E. Areces and Juan Heguiabehere, U Amsterdam, The Netherlands
HyLoRes 1.0: Direct resolution for hybrid logics

Simon Colton, U Edinburgh, UK
System description: The HR program for theorem generation

Joe Hurd, U Cambridge, UK
An LCF-style interface between HOL and first-order logic

Mateja Jamnik, U Cambridge, UK; Manfred Kerber, U Birmingham, UK; and Martin Pollet, Saarland U, Germany
LearnOmatic: System description

Michael Kohlhase, Carnegie Mellon U, USA and Jürgen Zimmer, Saarland U, Germany
System description: The MathWeb software bus for distributed mathmatical reasoning

Jesper Møller, IT U of Copenhagen, Denmark
DDDLIB: A library for solving quantified difference inequalities

Stephan Schulz, Techn. U of Munich, Germany and Geoff Sutcliffe, U Miami, USA
System description: GrAnDe 1.0

Jörg Siekmann, Saarland U, Germany et al.
Proof development with OMEGA

Christoph Weidenbach, Opel AG, Germany; Uwe Brahm, MPI Saarbrücken, Germany; Thomas Hillenbrand, MPI Saarbrücken, Germany; Enno Keen, MPI Saarbrücken, Germany; Christian Theobalt, MPI Saarbrücken, Germany; and Dalibor Topic, MPI Saarbrücken, Germany
SPASS version 2.0

Michael Whalen, U Minnesota, USA; Johann Schumann, NASA Ames, USA; and Bernd Fischer, NASA Ames, USA
AutoBayes/CC - combining program synthesis with automatic code certification - system description