摘要：Real-world applications of automated theorem proving require modern software environments that enable modularisation, networked inter-operability, robustness, and scalability. These requirements are met by the Agent-Oriented Programming paradigm of Distributed Artificial Intelligence. We argue that a reasonable framework for automated theorem proving in the large regards typical mathematical services as autonomous agents that provide internal functionality to the outside and that, in turn, are able to access a variety of existing external services. This article describes the MathWeb architecture that encapsulates a wide range of traditional mathematical systems each into a social agent-shell. A communication language based on the Knowledge Query and Manipulation Language (KQML) is proposed in order to allow conversations between these mathematical agents. The individual speech acts of their conversations are about performances of the encapsulated services. The objects referred by these speech acts are mathematical objects, formulae in various log_ ics, and (partial) proofs in different calculi whose formalisation is done in an extension to the OpenMath standard. The result is a flexible framework for automated theorem proving which has already been implemented to a large extent in the context of the Omega proof development system.
