This course is the second part of a first year course of 18 lectures given in the Spring term by me and
Professor Sophia Drossopoulos.
My part consists of 8 lectures and covers the following topics: Binary Chop,
Partitions and Sorting,
Warshall's algorithm and
Tail Recursion You might find the following documents helpful (and fun). Please see CATE for problem sheets and answers.
Back to top
The course is offered in the Autumn term to fourth year students and MSc (MAC) and MSc(Specialism) students. Current Teaching
Reasoning about Programs
Notes (Spring 2009)
Question Sheets
First year topic - Automated reasoning
Automated Reasoning
Introductory material on clausal form and resolution,
The Davis Putnam and Model Generation methods 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 proving
These (older) notes amplify the lecture notes, but are not required reading for examination purposes
Please see CATE for problem sheets and answers.
Back to topPandora 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).