Automated Reasoning Group

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

Archive

Various relevant papers may be found amongst the lab technical reports. We also publish a selection of inspiring Theorem Proving Haiku.
  Long-term projects
HOL
Isabelle




Links
Lab Publications
Technical Reports
Search
Haiku
Last modified on Wed May 9 23:10:47 BST 2012 by ns441 | Privacy policy