Second-Order Quantifier Elimination

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

• Renate Schmidt - University of Manchester
• Wednesday 03 December 2008, 14:15-15:15
• Lecture Theatre 1, Computer Laboratory.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• se393's list

Note that ex-directory lists are not shown.