This course is Part II of a first year course of 18 lectures. Since 2012 it has been given by
Professor Sophia Drossopoulos.
My part consisted of 8 lectures and covered the following topics: Binary Chop,
Partitions and Sorting,
Warshall's algorithm and
Tail Recursion You might find the following documents helpful (and fun). This course was previously offered to fourth year students and MSc (MAC) and MSc(Specialism) students. It will not be given this session (2014/15).
It included a case study on reasoning in Ontologies (given by Graham Deane - 4 hours). The notes here are for the 2013/2014 session (Graham's notes were issued separately).
My 24 hours covered: These (older) notes amplify the lecture notes, but are not required reading for examination purposesCurrent Teaching
Reasoning about Programs (until 2011)
Notes (From Spring 2011)
First year topic - Automated reasoning
Automated Reasoning
Introductory material on clausal form and resolution,
The Davis Putnam method for propositional reasoning, Resolution,
Refinements of resolution, including Hyper-resolution and OTTER (eProver), Tableau methods, including Model Elimination and variations,
Paramodulation, Knuth-Bendix Completion methods in theorem provingBackground notes:
Lecture notes Spring 2014:
Back to top
Pandora is a teaching package for Natural Deduction used for first year students in the Department of Computing. There have been several versions of the tool. The one called Pandora below has been in use since 2003 and was constructed by Alex Summers, Jiefei Ma, Tom Wheedon and others. The tool implements the Boxproof method used in the first year logic course and mentioned in the book Reasoned Programming.
You can find a link to the book at Reasoned Programming and to a web version of Pandora at Run Pandora
A new version was constructed by first and second year UROP students in summers of 2007-2009 to include an additional tool Raptor, for reasoning about programs. This is now available and can be used either for reasoning or for logic proofs. NewPandora and its extension Raptor, devised by Dr Gabrielle Sinnadurai and me has been constructed by UROP students Robin Bennett, Charence Wong, Alykhan Tejani, Deena Pindoria, Azalea Raad, Navin Manesh, Jean Moschetta, Jannis Bulian and Anton Stefanek. The Raptor tool allows to construct proofs of partial correctness of programs. Raptor can be downloaded for trial use from New Raptor download page We hope we have ironed out most of the problems, but if you find problems you can email me. When you start Raptor you have the option of Raptor (the reasoning tool) or Pandora (the logic tool).