hide
Free keywords:
-
Abstract:
The hierarchic superposition calculus over a theory T, called 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) terminates on the transformed clause set, hence
constitutes 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 FOL fragment
plus a theory T, if every non-constant 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.