University of Cambridge > > Computer Laboratory Wednesday Seminars > Mechanising First-Order Logic: Technology, Decidability and Applications

Mechanising First-Order Logic: Technology, Decidability and Applications

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

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.

This talk is part of the Computer Laboratory Wednesday Seminars series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity