Our research group studies the development of computational methods that carry out some emulation of reasoning. This involves studying logic-based and other techniques that improve how some form of reasoning can be approximated by computation. One of our main activities involves the development and application of theorem provers.
Theorem proving presents a challenge for logicians and computer scientists alike, and mechanising logical reasoning efficiently is hard. Despite its difficulty, theorem proving is finding substantial application in the computerised verification of safety-critical systems -- that is, proving that vital systems behave according to some precise specification.
Related Groups and Meetings
Various relevant papers may be found amongst the lab technical reports.
We also publish a selection of inspiring Theorem Proving Haiku.