Using symbolic computation in an automated sequent derivation

This paper presents a way in which symbolic computation can be used in automated theorem provers and specially in a system for automated sequent derivation in multi-valued logic. As an example of multi-valued logic, an extension of Post's Logic with linear order is considered. The basic ideas and main algorithms used in this system are presented. One of the important parts of the derivation algorithm is a method designed to recognize axioms of a given logic. This algorithm uses a symbolic computation method for establishing the solvability of systems of linear inequalities of special type. It will be shown that the algorithm has polynomial cost.