First order LUB approximations: characterization and algorithms

One of the major approaches to approximation of logical theories is the upper and lower bounds approach introduced by Selman and Kautz (1991, 1996). In this paper, we address the problem of lowest upper bound (LUB) approximation in a general setting. We characterize LUB approximations for arbitrary target languages, both propositional and first order, and describe algorithms of varying generality and efficiency for all target languages, proving their correctness. We also examine some aspects of the computational complexity of the algorithms, both propositional and first order; show that they can be used to characterize properties of whole families of resolution procedures; discuss the quality of approximations; and relate LUB approximations to other approaches existing in the literature which are not typically seen in the approximation framework, and which go beyond the “knowledge compilation” perspective that led to the introduction of LUBs.