Integration of automated reasoning and computer algebra systems

This Special Issue was initiated for the occasion of the Symposium on the Integration of Symbolic Computation Systems and Mechanized Reasoning—Calculemus 2002, which was held in Marseille, France, on July 1–5, 2002. It marked the 10th meeting of researchers from a community which is concerned with the design of mathematical software systems and computer-aided verification tools that base their strength on the interplay of deduction and computation provided by deduction and computer algebra systems, respectively. By its nature, the Calculemus community is itself a combined mix of experts in computer algebra and theorem proving, thus reaching a wide group of researchers in Symbolic Computation. The articles compiled in this Special Issue, some of which are extended versions of papers selected from contributions to Calculemus 2002, tackle core problems in the Calculemus mission goals. The paper of Armando and Ballarin on A reconstruction and extension of Maple’s Assume facility via constraint contextual rewriting shows how it is possible to improve a computer algebra system by viewing some of its facilities as theorem proving techniques. A formal semantical interpretation for limit computations is the topic of the paper by Beeson and Wiedijk, which again shows how correctness of computer algebra may benefit from a formal approach by considering The meaning of infinity in calculus and computer algebra systems. As described in the contribution by Gottliebsen, Kelsey, and Martin, Hidden verification for computational mathematics, computer algebra systems may also directly benefit from invoking computational logic, for instance in the verification of side conditions when dealing with differential equations. The reverse direction, namely improving the computational functionalities of proof assistants by integrating computer algebra, is the topic of Delahaye and Mayero’s article on Dealing with algebraic expressions over a field in Coq using Maple. Finally, Colton’s contribution Automated Conjecture Making in Number Theory using HR, Otter and Maple shows how research in pure mathematics may be carried out using a combination of symbolic computation tools allowing one to generate conjectures and prove or disprove them. We would like to thank the authors for their contributions to this special issue and the referees for the time they devoted to a rigorous peer review. We are also very grateful to the publisher and editor of the Journal of Symbolic Computation for giving us the opportunity