Approximate entailment

Approximation techniques are widely used in many areas of Computer Science for dealing with polynomially intractable problems. The major difficulty about introducing approximation in reasoning problems is in that it is very hard to find a measure of the approximation which is not dependent on the particular problem at hand. Our goal is to introduce the notion of approximate answers to reasoning problems which are known to be computationally intractable. We focus our attention on a reasoning problem which is both very general and computationally intractable: checking whether a propositional formula in Conjunctive Normal Form entails a clause. We present two sequences of entailment relations approximating the classical one: the relations of the first sequence are sound but not complete, while the relations of the second one are complete but not sound. Both sequences converge to classical entailment and can be computed in polynomial time under some conditions. Our claim is that both these sequences are an approximation of the entailment relation, since they always provide information clearly related to the original problem. In the last part of the paper, we sketch an algorithm for computing incrementally relations of the two sequences