Critical Agents Supporting Interactive Theorem Proving

We introduce a resource adaptive agent mechanism which supports the user of an interactive theorem proving system. The mechanism, an extension of 5 , uses a two layered architecture of agent societies to suggest applicable commands together with appropriate command argument instantiations. Experiments with this approach show that its e ectiveness can be further improved by introducing a resource concept. paper we provide an abstract view on the overall mechanism, motivate the necessity of an appropriate resource concept and discuss its realization within the agent architecture.

• Type: Conference
• Year: 1999
• Where: EPIA
• Authors: Christoph Benzmüller, Volker Sorge
• Keywords: Adaptive Agent Mechanism, Appropriate Command Argument, Artificial Intelligence, EPIA 1999, Resource Concept