2004b, ‘Towards polynomial approximations of full proposi- tional logic

Abstract. The aim of this paper is to study a family of logics that ap-proximates classical inference, in which every step in the approximation can be decided in polynomial time. For clausal logic, this task has been shown to be possible by Dalal [4, 5]. However, Dalal's approach cannot be applied to full classical logic. In this paper we provide a family of logics, called Limited Bivaluation Logics, via a semantic approach to approx-imation that applies to full classical logic. Two approximation families are built on it. One is parametric and can be used in a depth-rst ap-proximation of classical logic. The other follows Dalal's spirit, and with a dierent technique we show that it performs at least as well as Dalal's polynomial approach over clausal logic.