BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Second-Order Quantifier Elimination - Renate Schmidt - University 
 of Manchester
DTSTART:20081203T141500Z
DTEND:20081203T151500Z
UID:TALK13658@talks.cam.ac.uk
CONTACT:Mateja Jamnik
DESCRIPTION:In the investigation of logical methods and their application 
 in Computer Science\, and other fields\, there is a tension between\, on t
 he one hand\, the need for representational languages strong enough to exp
 ressively capture domain knowledge\, the need for logical formalisms gener
 al enough to provide several reasoning facilities relevant to the applicat
 ion\, and on the other hand\, the need to ensure reasoning facilities are 
 computationally feasible.  Second-order logics are very expressive and all
 ow 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 tha
 t make second-order logics computationally unfriendly. It is therefore des
 irable to eliminate these second-order quantifiers\, when this is mathemat
 ically possible\; and often it is. If second-order quantifiers are elimina
 ble we want to know under which conditions\, we want to understand the pri
 nciples and we want to develop methods for second-order quantifier elimina
 tion.\n\nIn this talk we introduce the problem of second-order quantifier 
 elimination and discuss two existing methods which have been automated: di
 rect methods based on a result of Ackermann and clausal methods based on s
 aturation 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 automatical
 ly solve the correspondence problem for large classes of modal axioms and 
 rules.\n
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR