An Improvement on Sub-Herbrand Universe Computation
Lifeng He1, *, †, Yuyan Chao2, *, †, Kenji Suzuki3, Zhenghao Shi 3, Hidenori Itoh 4
Identifiers and Pagination:Year: 2007
First Page: 12
Last Page: 18
Publisher Id: TOAIJ-1-12
Article History:Electronic publication date: 26/11/2007
Collection year: 2007
open-access license: This is an open access article distributed under the terms of the Creative Commons Attribution 4.0 International Public License (CC-BY 4.0), a copy of which is available at: (https://creativecommons.org/licenses/by/4.0/legalcode). This license permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.
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.