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.

论文关键词:Approximation,Reformulation,Knowledge compilation,Resolution theorem proving,Automated reasoning,First order logic

论文评审过程:Received 20 November 2001, Accepted 21 January 2004, Available online 13 December 2004.

论文官网地址:https://doi.org/10.1016/j.artint.2004.01.003