Skip to main content
SpringerLink
Log in
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Artificial Intelligence, Automated Reasoning, and Symbolic Computation (AISC 2002, Calculemus 2002)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2385))

  • 333 Accesses

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

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
    View author publications

    You can also search for this author in PubMed 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

Reprints 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

  • DOI: https://doi.org/10.1007/3-540-45470-5_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43865-6

  • Online ISBN: 978-3-540-45470-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation