880-01 Towards Learning New Methods inf Proff PlanningUsing Meta-variables for Natural Deducation in Theorema; Exploring Properties of Residue Classes; Defining Power Series and Polynomials in Mizar; Logic and Dependent Types in the Aldor Computer Algebra Systems; PART II: Invited Presentations; Communicating Mathematics on the Web; Teaching Mathematics Across the Internet; PART III: System Description; SINGULAR -A Computer Algebra System for Polynomial Computations; PART IV: Posters; Integration of Automated Reasoners: a Progress Report; Algorithmic Theories and Context
880-01/(S Cover; Half Title; Title Page; Copyright Page; Contents; PART I: Regular Contributions; Definite Integration of Parametric Rational Functions; How to Find Symmetries Hidden in Combinatorial Problem; Communication Protocols for Mathematical Services; Interfacing Computer Algebra and Deduction System; Development of the Theory of Continous Lattices in Mizar; Ω ANTS -Combining Interactive and Automated Theorem Proving; The THEOREMA Project: A Progress Report; How to Formally and Efficiently Prove Prime; On the EA-Style Integrated Processing of Self-Contained
The GiNaC Framework for Symbolic Computation ... A Framework for Prepositional Model Elimination Algorithms; Resource Guided Concurrent Deduction; Automated 'Plugging and Chugging'; Integrating SAT solvers with domain-specific reasoners; Solving Integrals at the Method Level; Lightweight Probability Theory for Verification; St Andrews CAAR Group: Poster Abstract; OpenXM -- an Open System to Integrate Mathematical Software; Presentation of the Foe project; Author Index; Authors' Affiliations
