A Blackboard Architecture for Guiding Interactive Proofs

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.

• Type: Conference
• Year: 1998
• Where: AIMSA
• Authors: Christoph Benzmüller, Volker Sorge
• Keywords: AIMSA 1998, Artificial Intelligence, Default Suggestion Mechanism, Default Suggestions, Theorem Proving Environments