A SEQUENT CALCULUS FOR AUTOMATED REASONING IN SYMBOLIC COMPUTATION SYSTEMS

In this paper the problem of reasoning on properties of mathematical o bjects 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 re sulting from computations. The main objective of this paper is to defi ne 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 aspe cts of the proposed automated reasoning apparatus are also discussed. Examples of execution are presented and possible further applications are hinted.