Quantification and Aggregation over Concepts of the Ontology

TL;DR

This paper introduces an extension to first-order logic for quantifying over concept sets in ontologies, enhancing knowledge representation with elaboration-tolerance and efficient well-formedness verification.

Contribution

It proposes a novel extension of FO(.) to support concept quantification, distinguishing it from second-order logic, and integrates this into the IDP-Z3 reasoning engine.

Findings

Extended FO(.) to support concept quantification

Achieved linear complexity in well-formedness verification

Improved modeling of problem domains with elaboration-tolerance

Abstract

We argue that in some KR applications, we want to quantify over sets of concepts formally represented by symbols in the vocabulary. We show that this quantification should be distinguished from second-order quantification and meta-programming quantification. We also investigate the relationship with concepts in intensional logic. We present an extension of first-order logic to support such abstractions, and show that it allows writing expressions of knowledge that are elaboration tolerant. To avoid nonsensical sentences in this formalism, we refine the concept of well-formed sentences, and propose a method to verify well-formedness with a complexity that is linear with the number of tokens in the formula. We have extended FO(.), a Knowledge Representation language, and IDP-Z3, a reasoning engine for FO(.), accordingly. We show that this extension was essential in accurately modelling various problem domains in an elaboration-tolerant way, i.e., without reification.