Inference in the FO(C) Modelling Language

TL;DR

This paper introduces a method for performing inference in the FO(C) logic by defining normal forms, transforming inference tasks to FO(ID), and implementing a prototype system, advancing understanding and capabilities in FO(C).

Contribution

It defines normal forms for FO(C), creates transformations to reduce inference to FO(ID), and implements the first inference system for FO(C).

Findings

Inference tasks in FO(C) can be reduced to FO(ID).

The prototype system performs inference in FO(C).

Complexity results for reasoning in FO(C) are provided.

Abstract

Recently, FO(C), the integration of C-Log with classical logic, was introduced as a knowledge representation language. Up to this point, no systems exist that perform inference on FO(C), and very little is known about properties of inference in FO(C). In this paper, we study both of the above problems. We define normal forms for FO(C), one of which corresponds to FO(ID). We define transformations between these normal forms, and show that, using these transformations, several inference tasks for FO(C) can be reduced to inference tasks for FO(ID), for which solvers exist. We implemented a prototype of this transformation, and thus present the first system to perform inference in FO(C). We also provide results about the complexity of reasoning in FO(C).