Quantification and Aggregation over Concepts of the Ontology
This work addresses a specific issue in knowledge representation for applications requiring quantification over concepts, offering an incremental improvement over existing formalisms.
The paper tackles the problem of quantifying over sets of concepts in knowledge representation by extending first-order logic to support such abstractions, enabling elaboration-tolerant knowledge expressions without reification. It presents a method for verifying well-formedness with linear complexity in tokens and demonstrates the extension's essential role in accurately modeling various problem domains.
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.