Automated Deduction for Projection Elimination

We investigate semantic and algorithmic aspects of projection, a logic operation that provides a straightforward semantic account for tasks in knowledge representation which involve extraction or removal of the knowledge that concerns a given vocabulary. As a basis for applications and processing methods, we formally work out properties of projection. Projection is a generalization of predicate quantification. We consider first-order logic, extended by a projection operator. In analogy to "quantifier elimination", we call the central computational operation to process the projection operator "projection elimination". It means to compute for a given sentence with the projection operator an equivalent sentence in which it does not occur. Projection elimination can be performed by adapted theorem proving methods. We first develop such a method which operates by resolvent generation and extends a known method for second-order quantifier elimination by some new features. Many of the recent practically successful automated deduction systems can be regarded as tableau-based, including theorem provers and model generators for first-order logic, reasoners for modal and description logics, propositional satisfiability solvers, propositional knowledge compilers, and answer set programming systems for non-monotonic logics. This motivates the investigation of further methods for projection elimination that are based on tableau construction. We develop a tableau framework that represents projection elimination, certain kinds of knowledge compilation, and propositional satisfiability solving as differently parameterized instances of a single task. By means of this framework we show that the efficiency of computing tasks that combine knowledge compilation with projection elimination can be essentially improved, in comparison with current practice, by incorporating elimination to some degree into the compilation process. Our framework abstracts from differences in tableau construction methods that are inessential for the adaption to tasks like projection elimination and knowledge compilation. Nevertheless, it takes key techniques of practically successful systems explicitly into account, such as, for example, dependency directed backtracking, without resorting to pseudocode. As a prototypical instantiation of the framework, we work out in detail an adaption of the Davis-Putnam-Logemann-Loveland procedure (DPLL) for projection elimination and knowledge compilation in propositional logic. DPLL is the basis of state-of-the-art propositional satisfiability solvers and can be regarded as tableau-based. Our DPLL adaption realizes the improvements of knowledge compilation by incorporation projection elimination that we have shown theoretically. It integrates many features that can be found dispersed in recent knowledge compilation methods based on DPLL or tableau techniques. It also can simulate a compilation method that is based on a different approach, the equivalence preserving rewriting of subformulas.