Definitions and (Uniform) Interpolants in First-Order Modal Logic

We first consider two decidable fragments of quantified modal logic S5: the one-variable fragment and its extension S5ALC that combines S5 and the description logic ALC with the universal role. As neither of them enjoys Craig interpolation or projective Beth definability, the existence of interpolants and explicit definitions of predicates---which is crucial in many knowledge engineering tasks---does not directly reduce to entailment. Our concern therefore is the computational complexity of deciding whether (uniform) interpolants and definitions exist for given input formulas, signatures and ontologies. We prove that interpolant and definition existence in the one-variable fragment of quantified modal logic S5 and in S5ALC is decidable in coN2ExpTime, being 2ExpTime-hard, while uniform interpolant existence is undecidable. Then we show that interpolant and definition existence in the one-variable fragment of quantified modal logic K is nonelementary decidable, while uniform interpolant existence is undecidable.