Resource Adaptive Agents in Interactive Theorem Proving

TL;DR

This paper presents a resource adaptive agent system for interactive theorem proving, enhancing user support by integrating resource management into a layered agent architecture to improve command suggestion effectiveness.

Contribution

It introduces a novel resource adaptive mechanism within a layered agent architecture for interactive theorem proving, emphasizing the importance of resource concepts.

Findings

Resource concept improves agent effectiveness

Layered architecture supports command suggestion

Abstract and practical insights into resource integration

Abstract

We introduce a resource adaptive agent mechanism which supports the user in interactive theorem proving. The mechanism uses a two layered architecture of agent societies to suggest appropriate commands together with possible command argument instantiations. Experiments with this approach show that its effectiveness can be further improved by introducing a resource concept. In this 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.