T-resolution: refinements and model elimination

T-resolution is a binary rule, proposed by Policriti and Schwartz in 1995 for theorem proving in first-order theories (T-theorem proving) that can be seen - at least at the ground level - as a variant of Stickel's theory resolution. In this paper we consider refinements of this rule as well as the model elimination variant of it. After a general discussion concerning our viewpoint on theorem proving in first-order theories and a brief comparison with theory resolution, the power and generality of T-resolution are emphasized by introducing suitable linear and ordered refinements, uniformly and in strict analogy with the standard resolution approach. Then a model elimination variant of T-resolution is introduced and proved to be sound and complete; some experimental results are also reported. In the last part of the paper we present two applications of T-resolution: to constraint logic programming and to modal logic.