Skip to main content
SpringerLink
Log in

System Description: inka 5.0 - A Logic Voyager

  • Conference paper
  • First Online:
Automated Deduction — CADE-16 (CADE 1999)

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

Included in the following conference series:

Abstract

Originally developed as an automatic inductive theorem prover [2] based on res- olution and paramodulation, the inka system was redesigned in inka 4.0 in the early ’90s [8] to meet the requirements arising from its designated use in formal methods. Meanwhile several large industrial applications of the verication sup- port environment (VSE) [7] have been performed which gave rise to thousands of proof obligations to be tackled by its underlying deductive system inka.

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. C. Benzmüller et al.: MEGA: Towards a mathematical assistant, In W. McCune (ed), CADE-14, Springer, LNAI 1249, 1997.

    Google Scholar 

  2. S. Biundo, B. Hummel, D. Hutter, C. Walther: The Karlsruhe Induction Theorem Proving System. In Jörg H. Siekmann (ed), CADE-8, Springer, LNCS 230, 1986.

    Google Scholar 

  3. CoFi-task group on language design, ESPRIT working group 29432, EU, 1998. CoFI Webpage: http://www.brics.dk/Projects/CoFI/

  4. L. Damas, R. Milner: Principal type schemes for functional programs, Ann. ACM Symp. on Principles of Programming Languages (POPL), 1982.

    Google Scholar 

  5. R. Harper, F. Honsell, G. Plotkin: A framework for defining logics, Journal of the Association for Computing Machinery, 40(1), 1993.

    Google Scholar 

  6. D. Hutter, M. Kohlhase: Managing Structural Information by Higher-Order Colored Unification, Journal of Automated Reasoning, accepted, 1999.

    Google Scholar 

  7. D. Hutter et al.: Verification Support Environment (VSE), Journal of High Integrity Systems, Vol. 1, 1996.

    Google Scholar 

  8. D. Hutter, C. Sengler: inka-The Next Generation. In M. McRobbie, J. Slaney (ed), CADE-13, Springer, LNAI 1104, 1996.

    Google Scholar 

  9. D. Hutter: Guiding Induction Proofs, In M. Stickel (ed), CADE-10, Springer, LNAI 449, 1991.

    Google Scholar 

  10. D. Hutter: Coloring terms to control equational reasoning, Journal of Automated Reasoning, Vol. 18, 1997.

    Google Scholar 

  11. Programming System Lab, Saarland University, Saarbrücken, 1998. The Oz Webpage: http://www.ps.uni-sb.de/ns3/oz/

  12. L.C. Paulson: Isabelle, A Generic Theorem Prover, Springer, LNCS 828, 1994.

    Google Scholar 

  13. J. Siekmann et al.: A Distributed Graphical User Interface for the Interactive Proof System MEGA. In R. C. Backhouse (ed), UITP98, Eindhoven Technical University, Report 98-08, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Saarland University, Postfach 15 11 50, D-66041, Saarbrücken, Germany

    Serge Autexier

  2. German Research Center for Artificial Intelligence, Stuhlsatzenhausweg 3, D-66123, Saarbrücken, Germany

    Dieter Hutter, Heiko Mantel & Axel Schairer

Authors
  1. Serge Autexier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dieter Hutter
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Heiko Mantel
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Axel Schairer
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Autexier, S., Hutter, D., Mantel, H., Schairer, A. (1999). System Description: inka 5.0 - A Logic Voyager. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-48660-7_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66222-8

  • Online ISBN: 978-3-540-48660-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation