A Sequent Calculus for Automated Reasoning in Symbolic Computation Systems

In this paper the problem of reasoning on properties of mathematical objects is considered in the context of symbolic computation. Automated reasoning mechanisms are proposed as a new basic computing tool in a symbolic computation system. These mechanisms are aimed to support the semantical correctness of a computation by allowing for verification of properties of mathematical objects introduced in the system and for generation and abduction of new properties of mathematical objects resulting from computations. The main objective of this paper is to define an extended sequent calculus to deal with generative and abductive logic problems, as well as with verificative problems, within a single methodological and computational environment. The implementation aspects of the proposed automated reasoning apparatus are also discussed. Examples of execution are presented and possible further applications are hinted.