7. Conclusions

Abstract

In Chapter 4 various theory connection calculi were described and related to each other. This comparison was concluded with the partial theory model elimination version and its restart variant as the most restricted versions. These calculi then were combined with the framework of theory inference rules. An abstract completeness criterion for theory inference rules was formulated, such that the combination with the foreground calculi is complete. Moreover, answer completeness result were obtained. Answer completeness generalises refutational completeness and is relevant for problem solving applications and, in the case of the restart variant, for disjunctive logic programming purposes. I consider these completeness results as the main results for Chapter 4.