Distributed First Order Logic

TL;DR

This paper provides a comprehensive, revised formal framework for Distributed First Order Logic (DFOL), including a sound and complete axiomatisation, to better represent and reason about distributed, heterogeneous knowledge systems.

Contribution

It offers a systematic, extended version of DFOL with a formal axiomatisation, addressing previous gaps and enhancing its applicability for distributed knowledge representation.

Findings

Systematic description of an extended DFOL framework.

A sound and complete axiomatisation based on Natural Deduction.

Enhanced formal tool for reasoning about distributed knowledge.

Abstract

Distributed First Order Logic (DFOL) has been introduced more than ten years ago with the purpose of formalising distributed knowledge-based systems, where knowledge about heterogeneous domains is scattered into a set of interconnected modules. DFOL formalises the knowledge contained in each module by means of first-order theories, and the interconnections between modules by means of special inference rules called bridge rules. Despite their restricted form in the original DFOL formulation, bridge rules have influenced several works in the areas of heterogeneous knowledge integration, modular knowledge representation, and schema/ontology matching. This, in turn, has fostered extensions and modifications of the original DFOL that have never been systematically described and published. This paper tackles the lack of a comprehensive description of DFOL by providing a systematic account of a completely revised and extended version of the logic, together with a sound and complete axiomatisation of a general form of bridge rules based on Natural Deduction. The resulting DFOL framework is then proposed as a clear formal tool for the representation of and reasoning about distributed knowledge and bridge rules.