Invited Papers.- George Boole, a Forerunner of Symbolic Computation.- Artificial Intelligence as a Decision Tool for Efficient Strategic and Operational Management.- OMDoc: Towards an Internet Standard for the Administration, Distribution, and Teaching of Mathematical Knowledge.- Contributed Papers and Poster Summaries.- On Communicating Proofs in Interactive Mathematical Documents.- Composite Distributive Lattices as Annotation Domains for Mediators.- A Proof Strategy Based on a Dual Representation.- Formalizing Rewriting in the ACL2 Theorem Prover.- Additional Comments on Conjectures, Hypotheses, and Consequences in Orthocomplemented Lattices.- Reasoning about the Elementary Functions of Complex Analysis.- Solving Nonlinear Systems by Constraint Inversion and Interval Arithmetic.- Basic Operators for Solving Constraints via Collaboration of Solvers.- Automatic Determination of Geometric Loci. 3D-Extension of Simson-Steiner Theorem.- Numerical Implicitization of Parametric Hypersurfaces with Linear Algebra.- A Note on Modeling Connectionist Network Structures: Geometric and Categorical Aspects.- A New Artificial Intelligence Paradigm for Computer-Aided Geometric Design.- How Symbolic Computation Can Benefit Computer-Aided Geometric Design.- CDR: A Rewriting Based Tool to Design FPLA Circuits.- Locally Effective Objects and Artificial Intelligence.- Negotiation Algorithms for Multi-agent Interactions.- Some Techniques of Isomorph-Free Search.