Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

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

  • Conference paper
  • First Online:

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.

This is a preview of subscription content,log in via an institution to check access.

Access this chapter

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. A.S. Karpenko, Multivalued logics. Logic and Computer. Issue 4, Moscow, Nauka, 1997.

    Google Scholar 

  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. 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. R. Tarjan, Depth First Search and Linear Graph Algorithms, SIAM J. Computing 1 (1972), 146–160

    Article MATH MathSciNet  Google Scholar 

  5. R. Tarjan, Data Structures and Network Algorithms, SIAM Philadelphia,(1983) 71–95

    Google Scholar 

  6. Gerberding S. Deep Thought. University of Darmstadt, Dept. of Computer Science, 1996.

    Google Scholar 

  7. Lowerence C. Paulson. Designing a theorem Prover. Oxford, 1995. pp. 416–476.

    Google Scholar 

  8. Michael J. Panik. Linear Programming: Mathematics, Theory and Algorithms. Kluwer Academic Publishers, 1996. pp.125–139.

    Google Scholar 

  9. L.G. Hachiyan, A polinomial algorithm in linear programming, Soviet Mathematics Doclady 20,(1979), pp. 191–194.

    Google Scholar 

  10. Jorge Nocedal, Stephen J. Wright. Numerical Optimization, Springer, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Ontario Research Center for Computer Algebra, University of Western Ontario, London, Ontario, Canada, N6A 5B7

    Elena Smirnova

Authors
  1. Elena Smirnova

    You can also search for this author inPubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Karlsruhe (TH), Am Fasanengarten 5, Postfach 6980, D-76128, Karlsruhe, Germany

    Jacques Calmet

  2. CMI, Université de Provence, 39 rue F. Juliot-Curie, 13453, Marseille Cedex 13, France

    Belaid Benhamou

  3. Research Institute for Symbolic Computation (RISC-Linz), Johannes Kepler University, A-4040, Linz, Austria

    Olga Caprotti

  4. ESIL, Université de la Méditerannée, 163 Avenue de Luminy, Marseille Cedex 09, France

    Laurent Henocque

  5. School of Computer Science, University of Birmingham, Birmingham, B15 2TT, UK

    Volker Sorge

Rights and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Smirnova, E. (2002). Using Symbolic Computation in an Automated Sequent Derivation System for Multi-valued Logic. In: Calmet, J., Benhamou, B., Caprotti, O., Henocque, L., Sorge, V. (eds) Artificial Intelligence, Automated Reasoning, and Symbolic Computation. AISC Calculemus 2002 2002. Lecture Notes in Computer Science(), vol 2385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45470-5_9

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp