Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A blackboard architecture for guiding interactive proofs

  • Conference paper
  • First Online:
Artificial Intelligence: Methodology, Systems, and Applications (AIMSA 1998)

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

Abstract

The acceptance and usability of current interactive theorem proving environments is, among other things, strongly influenced by the availability of an intelligent default suggestion mechanism for commands. Such mechanisms support the user by decreasing the necessary interactions during the proof construction. Although many systems offer such facilities, they are often limited in their functionality. In this paper we present a new agent-based mechanism that independently observes the proof state, steadily computes suggestions on how to further construct the proof, and communicates these suggestions to the user via a graphical user interface. We furthermore introduce a focus technique in order to restrict the search space when deriving default suggestions. Although the agents we discuss in this paper are rather simple from a computational viewpoint, we indicate how the presented approach can be extended in order to increase its deductive power.

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. P. B. Andrews. An Introduction To Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, San Diego, CA, USA, 1986.

    Google Scholar 

  2. P. B. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning, and H. Xi. Tps: A Theorem Proving System for Classical Type Theory. Journal of Automated Reasoning, 16(3):321–353, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  3. C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann, and V. Sorge. ΩMega: Towards a Mathematical Assistant. In W. McCune, editor, Proceedings of the 14th Conference on Automated Deduction (CADE-14), LNAI, Townsville, Australia, 1997. Springer Verlag, Berlin, Germany.

    Google Scholar 

  4. R. Engelmore and T. Morgan, editors. Blackboard Systems. Addison-Wesley, 1988.

    Google Scholar 

  5. L. D. Erman, F. Hayes-Roth, and R. D. Reddy. The HERSAY-II speech understanding system: Integrating knowledge to resolve uncertainty. ACM Computing Surveys, 12(2), 1980.

    Google Scholar 

  6. L. Erman, P. London, and S. Fickas. The Design and an Example Use of HEARSAY-III. In P. J. Hayes, editor, Proceedings of the 7th International Joint Conference on Artificial Intelligence (IJCAI '81), pages 409–415. William Kaufmann, 1981.

    Google Scholar 

  7. G. Gentzen. Untersuchungen über das Logische Schlie\en I und II. Mathematische Zeitschrift, 39:176–210, 405–431, 1935.

    Article  MathSciNet  Google Scholar 

  8. M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge University Press, Cambridge, United Kingdom, 1993.

    Google Scholar 

  9. M. A. Pérez and J. L. Sibert. Focus in graphical user interfaces. In W. D. Gray, William E. Hefley, and Dianne Murray, editors, Proceedings of the International Workshop on Intelligent User Interfaces, pages 255–258. ACM Press, 1993.

    Google Scholar 

  10. The Oz Programming System Programming Systems Lab, DFKI, Germany, 1998. URL: http://www.ps.uni-sb.de/oz/.

    Google Scholar 

  11. J. Siekmann, S. M. Hess, C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, M. Kohlhase, K. Konrad, E. Melis, A. Meier, and V. Sorge. LΩUI: A Distributed Graphical User Interface for the Interactive Proof System Ω mega. Submitted to the International Workshop on User Interfaces for Theorem Provers, 1998.

    Google Scholar 

  12. J. W. Sullivan and S. W. Tyler, editors. Intelligent User Interfaces. ACM Press Frontier Series. ACM Press, New York, NY, USA, 1991.

    Google Scholar 

  13. L. Théry, Y. Bertot, and G. Kahn. Real Theorem Provers Deserve Real User-Interfaces. In Proceedings of The Fifth ACM Symposium on Software Development Environments (SDE5), Washington D.C., USA, December 1992. ACM Press.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität des Saarlandes, D-66123, Saarbrücken, Germany

    Christoph Benzmüller & Volker Sorge

Authors
  1. Christoph Benzmüller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Volker Sorge
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Fausto Giunchiglia

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Benzmüller, C., Sorge, V. (1998). A blackboard architecture for guiding interactive proofs. In: Giunchiglia, F. (eds) Artificial Intelligence: Methodology, Systems, and Applications. AIMSA 1998. Lecture Notes in Computer Science, vol 1480. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0057438

Download citation

  • DOI: https://doi.org/10.1007/BFb0057438

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64993-9

  • Online ISBN: 978-3-540-49793-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation