Mechanising First-Order Logic: Technology, Decidability and Applications

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

• Christoph Weidenbach, Max Planck Institut
• Wednesday 31 January 2007, 14:15-15:15
• Lecture Theatre 1, Computer Laboratory.

If you have a question about this talk, please contact Timothy G. Griffin.

Starting from Robinson’s resolution principle I will develop the superposition framework for first-order logic. Superposition is the most promising candidate framework for the mechanisation of first-order logic today. It enables the development of efficient decision procedures for a variety of classical decidable subclasses of first-order logic, as well as the detection of new decidable classes. If the first-order formalisation of an application domain falls into a decidable class, or gets close to it, we very often can provide a scalable and efficient tool for the analysis/verification of properties. Example domains are security protocols, LAN infrastructures, data structures or transition systems.

http://www.mpi-sb.mpg.de/~weidenb/

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.