Polynomial approximations of full propositional logic via limited bivalence

Abstract

The aim of this paper is to study an anytime family of logics that approximates 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 [Dal96a,Dal96b]. However, Dalal's approach cannot be applied to full classical logic. In this paper we provide a family of logics, called Limited Bivalence Logics, that approximates full classical logic. Our approach contains two stages. In the first stage, a family of logics parameterised by a set of formulas Σ is presented. A lattice-based semantics is given and a sound and complete tableau-based proof-theory is developed. In the second stage, the first family is used to create another approximation family, in which every approximation step is shown to be polynomially decidable.