Distributed First Order Logic

In this paper we define a logic, called \emph{Distributed First Order Logic (DFOL)}, for the formalization of distributed knowledge-based systems. In these systems knowledge is distributed in a set of heterogeneous subsystems. Each subsystem represents, in its own language, partial knowledge about a subset of the whole domain, and is able to exchange knowledge with the other subsystems via query answering. DFOL formalizes the partial knowledge of each subsystem by means of a first order theory on a given domain, and represents the semantic overlapping between subsystems by means of relations between formulas in the languages of the different subsystems and relations between objects in their domains. In this paper we present the syntax and semantics of DFOL. Moreover we provide a sound and complete calculus, based on natural deduction, for DFOL