University of Cambridge > > Wednesday Seminars - Department of Computer Science and Technology  > Second-Order Quantifier Elimination

Second-Order Quantifier Elimination

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Mateja Jamnik.

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.

This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity