Abstract is missing.
- Interactive Theorem Proving and Computer AlgebraJohannes Ueberberg. 1-9
- A Practical Algorithm for Geometric Theorem ProvingAshutosh Rege, John F. Canny. 10-17
- Combining Theorem Proving and Symbolic Mathematical ComputingKarsten Homann, Jacques Calmet. 18-29
- Tools for Solving Problems in the Scope of Algebraic ProgrammingY. V. Kapitonova, Alexander A. Letichevsky, Vladislav A. Volkov, M. S. Lvov. 30-47
- Planning a Proof of the Intermediate Value TheoremMyles Chippendale. 48-63
- A General Technique for Automatically Optimizing Programs Through the Use of Proof PlansPeter Madden, Ian Green. 64-79
- Datalog and TwoGroups and C++Gregory Butler. 80-92
- Linear Logic and Real Closed Fields: a Way to Handle Situations DynamicallyPierre Jumpertz. 93-114
- A Proof Environment for Arithmetic with the Omega RuleSiani Baker, Alan Smaill. 115-130
- Using Commutativity Properties for Controlling CoercionsStephan A. Missura, Andreas Weber. 131-143
- Theories = Signatures + Propositions Used as TypesStephan A. Missura. 144-155
- The Ideal Structure of Gröbner Base ComputationsStéphane Collart, Daniel Mall. 156-166
- Modeling Cooperating Agents Scenarios by Deductive Planning Methods and Logical FiberingsJochen Pfalzgraf, Ute Cornelia Sigmund, Karel Stokkermans. 167-190
- Propagation of Mathematical Constraints in Subdefinite ModelsVitaly Telerman. 191-208
- Combining Computer Algebra and Rule Based ReasoningReinhard Bündgen. 209-223
- Algebraic Specification of Empirical Inductive Learning Methods based on Rough Sets and Matroid TheoryShusaku Tsumoto, Hiroshi Tanaka. 224-243
- Subsymbolic Processing using Adaptive AlgorithmsDavid J. Nettleton, Roberto Garigliano. 244-254
- An Interpretation of the Propositional Boolean Algebra as k-algebra. Effective CalculusLuis M. Laita, Luis de Ledesma, Eugenio Roanes-Lozano, Eugenio Roanes-Macías. 255-263
- Subdefinite Computations and Symbolic Transformations in the UniCalc SolverAlexander Semenov, Alexander Babichev, Alexander Leshchenko. 264-275