On the Complexity of Model Expansion

Abstract. We study the complexity of model expansion (MX), which is the problem of expanding a given finite structure with additional relations to produce a finite model of a given formula. This is the logical task underlying many practical constraint languages and systems for representing and solving search problems, and our work is motivated by the need to provide theoretical foundations for these. We present results on both data and combined complexity of MX for several fragments and extensions of FO that are relevant for this purpose, in particular the guarded fragment GFk of FO and extensions of FO and GFk with inductive definitions. We present these in the context of the two closely related, but more studied, problems of model checking and finite satisfiability. To obtain results on FO(ID), the extension of FO with inductive definitions, we provide translations between FO(ID) with FO(LFP), which are of independent interest.

• Type: Journal
• Year: 2010
• Where: LPAR
• Authors: Antonina Kolokolova, Yongmei Liu, David G. Mitchell, Eugenia Ternovska
• Keywords: Automated Reasoning, Inductive Definitions, LPAR 2010, Model, Practical Constraint Languages