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)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  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–160zbMATHCrossRefMathSciNetGoogle Scholar
  5. [5]
    R. Tarjan, Data Structures and Network Algorithms, SIAM Philadelphia,(1983) 71–95Google Scholar
  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

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Elena Smirnova
    • 1
  1. 1.Ontario Research Center for Computer AlgebraUniversity of Western OntarioLondonCanada

Personalised recommendations