Skip to main content
SpringerLink
Log in

INKA: The next generation

  • Session 4B
  • Conference paper
  • First Online:
Automated Deduction — Cade-13 (CADE 1996)

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

Included in the following conference series:

Abstract

The INKA system is a first-order theorem prover with induction based on the explicit induction paradigm. Since 1986 when a first version of the INKA system was developed there have been many improvements. In this description we will give a short overview of the current system state and its abilities.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. D. Hutter, B. Langenstein, C. Sengler, J. Siekmann, W. Stephan, and A. Wolpers. Deduction in the Verification Support Environment (VSE). Proceedings of the Formal Methods Europe 96, Oxford, Great Britain, 1996.

    Google Scholar 

  2. S. Biundo, B. Hummel, D. Hutter, and C. Walther. The Karlsruhe Induction Theorem Proving System. In J. H. Siekmann, editor, Proceedings 8th International Conference on Automated Deduction (CADE), Lecture Notes in Computer Science (LNCS) 230, Oxford, England, 1986. Springer-Verlag, Berlin, Germany.

    Google Scholar 

  3. R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, London, England, 1979.

    Google Scholar 

  4. A. Bundy, A. Stevens, F. v. Harmelen, A. Ireland, and A. Smaill. Rippling: a heuristic for guiding inductive proofs. Journal of Artificial Intelligence, North Holland Publishing Company, pp. 185–253, No. 62, 1993.

    Google Scholar 

  5. J. Giesl. Automatisierung von Terminierungsbeweisen für rekursiv definierte Algorithmen. infix, 1995.

    Google Scholar 

  6. D. Hutter. Guiding Induction Proofs In M. Stickel, editor, Proceedings 10 th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence (LNAI) 449, Kaiserslautern, Germany, 1990, Springer-Verlag, Berlin, Germany.

    Google Scholar 

  7. D. Hutter. Adapting a Resolution Calculus for Inductive Proofs. In B. Neumann, editor, 10th European Conference on Artificial Intelligence, pages 65–69. Wiley and sons, 1992.

    Google Scholar 

  8. D. Hutter. Colouring Terms to Control Equational Reasoning Journal of Automated Reasoning, Kluwer, forthcoming.

    Google Scholar 

  9. C. Sengler. Termination of Algorithms over Non-Freely Generated Data Types. Proceedings 13th International Conference on Automated Deduction (CADE), 1996.

    Google Scholar 

  10. C. Walther. On proving the termination of algorithms by machine. Artificial Intelligence, 71, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Dieter Hutter & Claus Sengler

Authors
  1. Dieter Hutter
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Claus Sengler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

M. A. McRobbie J. K. Slaney

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hutter, D., Sengler, C. (1996). INKA: The next generation. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_92

Download citation

  • DOI: https://doi.org/10.1007/3-540-61511-3_92

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-68687-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation