ion Within Partial Deduction for Linear Logic . . . . . . . . . . . . . . . . . 52 P. K¨ungas A Decision Procedure for Equality Logic with Uninterpreted Functions . . . 66 O. Tveretina Generic Hermitian Quantifier Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 A. Dolzmann and L.A. Gilch Extending Finite Model Searching with Congruence Closure Computation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 J. Zhang and H. Zhang On the Combination of Congruence Closure and Completion . . . . . . . . . . . . 103 C. Scharff and L. Bachmair Combination of Nonlinear Terms in Interval Constraint Satisfaction Techniques . . . . . . . . . . . . . . . . . . . . . . . . . 118 L. Granvilliers and M. Ouabiba Proving and Constraint Solving in Computational Origami . . . . . . . . . . . . . . 132 T. Ida, D. T¸epeneu, B. Buchberger, and J. Robu An Evolutionary Local Search Method for Incremental Satisfiability . . . . . . 143 M. El Bachir Mena¨ı