|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Second-Order Quantifier Elimination
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 Computer Laboratory Wednesday Seminars series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listsOWASP (Application Security) Cambridge Chapter Events & Conferences CAMSED OCaml Labs Events
Other talksRecent Advances in Molecular and Cellular Pathology Cambridge Statistics Clinic Easter III Computational Neuroscience Journal Club C-type lectins and the control of Immunity ‘Rising Powers in the Western Imagination’ Pfizer Neusentis Graduate and Young Academics Symposium