SUP(T) decides first-order logic fragment over ground theories

摘要

The hierarchic superposition calculus SUP (T) enables sound reasoning on the hierarchic combination of a theory T with full first-order logic FOL(T). If a FOL(T) clause set enjoys a sufficient completeness criterion, the calculus is even complete. Clause sets over the ground fragment of FOL (T) are not sufficiently complete, in general. In this paper we show that any clause set over the ground FOL(T) fragment can be transformed into a sufficiently complete one, and prove that SUP(T) is terminating for the transformed clause set, hence a decision procedure provided the existential fragment of the theory T is decidable. Thanks to the hierarchic design of SUP(T), the decidability result can be extended beyond the ground case. We show SUP (T) is a decision procedure for the non-ground Horn FOL fragment plus a ground theory T, if every nonconstant function symbol from the underlying FOL signature ranges into the sort of the theory T, and every term of the theory sort is ground. Examples for T are in particular decidable fragments of arithmetic.