Computing with logic as operator elimination: The ToyElim system

Abstract. A prototype system is described whose core functionality is, based on propositional logic, the elimination of second-order opera-tors, such as Boolean quantifiers and operators for projection, forgetting and circumscription. This approach allows to express many representa-tional and computational tasks in knowledge representation – for exam-ple computation of abductive explanations and models with respect to logic programming semantics – in a uniform operational system, backed by a uniform classical semantic framework. 1 Computation with Logic as Operator Elimination We pursue an approach to computation with logic emerging from three theses: 1. Classical first-order logic extended by some second-order operators suffices to express many techniques of knowledge representation. Like the standard logic operators, second-order operators can be defined seman-tically, by specifying the requirements on an interpretation to be a model of a formula whose principal functor is the operator, depending only on seman