Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Distributed First Order Logic

Chiara Ghidini, Luciano Serafini

TL;DR

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.

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.

Distributed First Order Logic

TL;DR

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.

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.

Paper Structure

This paper contains 38 sections, 15 theorems, 74 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Two explanatory examples
  3. Reasoning with viewpoints
  4. Mediator-based Information Integration
  5. Syntax and Semantics of DFOL
  6. DFOL Syntax
  7. Denoting cross-domain objects
  8. DFOL Semantics
  9. Satisfiability and arrow variables
  10. Satisfiability in a set of local models
  11. Local inconsistency
  12. Denoting cross-KB constraints via bridge rules
  13. How to represent distributed knowledge via bridge rules
  14. Representing specific domain relations
  15. Representing semantic mappings
  16. ...and 23 more sections

Key Result

Proposition 1

Let $\overset{\rightarrow}{x}$ denote either $\overset{\rightarrow j}{ x}$ or $\overset{j\rightarrow}{x}$ for some $j\neq i$, and ${\cal{M}}\xspace$ be a DFOL model such that $M_i$ contains a single first-order model $m$. Then the following properties hold:

Figures (9)

  • Figure 1: The magic box.
  • Figure 2: An example of mediator system.
  • Figure 3: Denoting cross-domain objects in the magic box example.
  • Figure 4: Partial knowledge in the magic box.
  • Figure 5: Graphical representation of the properties of the domain relation.
  • ...and 4 more figures

Theorems & Definitions (45)

  • Example 1: The magic box
  • Example 2
  • Example 3: Languages for the magic box
  • Definition 1: Set of Local Models
  • Definition 2: Domain relation
  • Definition 3: DFOL Model
  • Example 4
  • Definition 4: Assignment
  • Definition 5: Admissible assignment
  • Definition 6: Satisfiability
  • ...and 35 more