Second-Order Quantifier Elimination

Second-Order Quantifier Elimination

Abstract

In the investigation of logical methods and their application in Computer Science, and other fields, there is a tension between, on the one hand, the need for representational languages strong enough to expressively capture domain knowledge, the need for logical formalisms general enough to provide several reasoning facilities relevant to the application, and on the other hand, the need to ensure reasoning facilities are computationally feasible. Second-order logics are very expressive and allow us to represent domain knowledge with ease, but there is a high price to pay for the expressiveness. Most second-order logics are incomplete and highly undecidable.

It is the quantifiers which bind relation symbols that make second-order logics computationally unfriendly. It is therefore desirable to eliminate these second-order quantifiers, when this is mathematically possible; and often it is. If second-order quantifiers are eliminable we want to know under which conditions, we want to understand the principles and we want to develop methods for second-order quantifier elimination. In this talk we introduce the problem of second-order quantifier elimination and discuss two existing methods which have been automated: direct methods based on a result of Ackermann and clausal methods based on saturation with resolution. Various examples of applications will be given. We focus in more detail on modal correspondence theory where second-order quantifier elimination methods are being successfully used to automatically solve the correspondence problem for large classes of modal axioms and rules.