An Improvement on Sub-Herbrand Universe Computation

ABSTRACT

This paper presents an efficient algorithm for computing sub-Herbrand universes for arguments of functions and predicates in a given clause set. Unlike the previous algorithm, which processes all clauses in the given clause set once for computing each sub-Herbrand universe, the proposed algorithm computes all sub-Herbrand universes in the clause set by processing each clause in the clause set only once. We prove the correctness of our algorithm, and we provide experimental results on theorem proving benchmark problems to show the power of our approach.