Distributed agent-based automated theorem proving in order-sorted first-order logic

TL;DR

This paper introduces a distributed agent-based framework for automated theorem proving in order-sorted first-order logic, emphasizing communication constraints and proof construction rather than performance evaluation.

Contribution

It presents a refutation-complete report procedure for theorem proving in a distributed setting with restricted communication between agents.

Findings

Provides a proof procedure for distributed theorem proving in order-sorted logic.

Ensures refutation completeness under communication restrictions.

Focuses on proof construction rather than performance metrics.

Abstract

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.