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.
Evgeny Kruglov Christoph Weidenbach
Universit(a)t des Saarlandes, Max-Planck-Institut für Informatik Campus El 4, D-66123 Saarbrücken
国际会议
北京
英文
126-148
2011-10-21（万方平台首次上网日期，不代表论文的发表时间）