Distributed First Order Logics

In distributed knowledge representation and reasoning systems, knowledge is represented by a set of heterogeneous subsystems, each of which autonomously represents and reasons about a certain subset of the whole knowledge. These subsystems are not completely independent on one another as the same piece of knowledge might be represented (from different points of view) in different subsystems. In this paper we provide a formalization of the relation between the knowledge contained in different subsystems. We define a formal logic, called Distributed First Order Logic (DFOL), which models relations between objects and relations between formulae of different subsystems. We provide a calculus (based on natural deduction) to reason about DFOL. DFOL syntax is composed of a family of first order languages, each of which represents a piece of the global knowledge. DFOL semantics is composed of a family of set of first order interpretations on a domain, one for each DFOL language, and a family of relations between the domains of each interpretation. DFOL calculus is composed of a set of first order natural deduction systems connected by a set of rules which allow to export theorems among different theories. We also provide a list of representational requirements and structural requirements for DFOL to be adequate and we show that DFOL satisfies them