  This paper presents a distributed agent-based automated theorem proving
framework based on order-sorted first-order logic. Each agent in our framework
has its own knowledge base, communicating to its neighboring agent(s) using
message-passing algorithms. The communication language between agents is
restricted in such a manner that each agent can only communicate to its
neighboring agent(s) by means of their common language. In this paper we
provide a refutation-complete report procedure for automated theorem proving in
order-sorted first-order logic in a subclass of distributed agent-based
networks. Rather than studying and evaluating the performance improvement of
the automated theorem proving in order-sorted first-order logic using parallel
or distributed agents, this paper focuses on building proofs in order-sorted
first-order logic in a distributed manner under the restriction that agents may
report their knowledge or observations only with their predefined language.
