# Using Symbolic Computation in an Automated Sequent Derivation System for Multi-valued Logic

• Elena Smirnova
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2385)

## Abstract

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.

## References

1. [1]
A.S. Karpenko, Multivalued logics. Logic and Computer. Issue 4, Moscow, Nauka, 1997.Google Scholar
2. [2]
Kossovski N.K., Tishkov A.V. Logical theory of Post Logic with linear order. TR-98-11, Department of Informatics University Paris-12. 9p.Google Scholar
3. [3]
N. Kossovski, A. Tishkov. Gradable Logical Values For Knowledge Representation. Notes of Scientific Seminars vol. 241 pp 135–149 St.Petersburg University 1996.Google Scholar
4. [4]
R. Tarjan, Depth First Search and Linear Graph Algorithms, SIAM J. Computing 1 (1972), 146–160
5. [5]
6. [6]
Gerberding S. Deep Thought. University of Darmstadt, Dept. of Computer Science, 1996.Google Scholar
7. [7]
Lowerence C. Paulson. Designing a theorem Prover. Oxford, 1995. pp. 416–476.Google Scholar
8. [8]
Michael J. Panik. Linear Programming: Mathematics, Theory and Algorithms. Kluwer Academic Publishers, 1996. pp.125–139.Google Scholar
9. [9]
L.G. Hachiyan, A polinomial algorithm in linear programming, Soviet Mathematics Doclady 20,(1979), pp. 191–194.Google Scholar
10. [10]
Jorge Nocedal, Stephen J. Wright. Numerical Optimization, Springer, 1999.Google Scholar