The program committee accepted 19 out of 24 regular papers, as well as 3 position papers.
Constraint Contextual Rewriting
Alessandro Armando, Silvio Ranise
How Complex is a Finite First-Order Sorted Interpretation?
Thierry Boy de la Tour
A Further and Effective Liberalization of the Delta-Rule in Free Variable Semantic Tableaux
Domenico Cantone, Marianna Nicolosi Asmundo
A new fast tableau-based decision procedure for an unquantified fragment of set theory
Domenico Cantone, Calogero G. Zarba
Interpretation of a Mizar-like Logic in First Order Logic
Ingo Dahn
An O((n.log n)^3)-time transformation from Grz into decidable fragments of classical first-order logic
Stephane Demri, Rajeev Gore
Implicational completeness of signed resolution
Christian Fermüller
An equational re-engineering of set theories
Andrea Formisano, Eugenio Omodeo
A Partial Instantiation based First Order Theorem Prover
J.N. Hooker, G. Rago, Vijay Chandru, Anjul Shrivastava
Issues of decidability for description logics in the framework of resolution
Ullrich Hustadt, Renate A. Schmidt
Upper bound to the height of terms in proofs with cuts
Boris Konev
Proof Generalization and Function Introduction
Nicolas Peltier
Extending Decidable Clause Classes via Constraints
Reinhard Pichler
Completeness and Redundancy in Constrained Clause Logic
Reinhard Pichler
Efficient proof-theoretical properties for some first order intuitionistic modal logics
Aida Pliuskeviciene
Hidden Congruent Deduction
Grigore Rosu, Joseph Goguen
Resolution-based Theorem Proving for SHn-Logics
Viorica Sofronie-Stokkermans
A new resolution calculus for the infinite-valued propositional logic of Lukasiewicz
Hubert Wagner
Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and theLiberalized Delta-Rule and Without Skolemization
Claus-Peter Wirth
Theorem proving strategies: a search oriented taxonomy
Maria Paola Bonacina
Computational Representations of Models of First-Order Formulas
Robert Matzinger
Position Paper: Verifying Textbook Proofs
Claus Zinn