Incremental theory reasoning methods for semantic tableaux

Abstract

Theory reasoning is an important technique for increasing the efficiency of automated deduction systems. In this paper we present incremental theory reasoning, a method that improves the interaction between the foreground reasoner and the background (theory) reasoner and, thus, the efficiency of the combined system. The use of incremental theory reasoning in free variable semantic tableaux and the cost reduction that can be achieved axe discussed; as an example, completion-based equality reasoning is presented, including experimental data obtained using an implementation.