BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Mechanising First-Order Logic: Technology\, Decidability and Appli
 cations - Christoph Weidenbach\, Max Planck Institut
DTSTART:20070131T141500Z
DTEND:20070131T151500Z
UID:TALK6262@talks.cam.ac.uk
CONTACT:Timothy G. Griffin
DESCRIPTION:Starting from Robinson's resolution principle I will develop t
 he superposition framework for\nfirst-order logic. Superposition is the mo
 st promising candidate framework for the mechanisation\nof first-order  lo
 gic today. It enables the development of efficient decision procedures for
  a variety of\nclassical decidable subclasses of first-order logic\, as we
 ll as the detection of new decidable\nclasses. If the first-order  formali
 sation of an application domain falls into a decidable class\,\nor gets cl
 ose to it\, we very often can provide a scalable and efficient tool for th
 e analysis/verification\nof properties. Example domains are security proto
 cols\, LAN infrastructures\, data structures or transition systems.\n\nhtt
 p://www.mpi-sb.mpg.de/~weidenb/
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR