Reasoning about Programs (until 2011)
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
Notes (From Spring 2011)
You might find the following documents helpful (and fun).
First year topic – Automated reasoning
The course was previously offered in the Autumn term to fourth year students and MSc (MAC) and MSc(Specialism) students. It will be in the Spring term this session (2013/14) and is being slightly revised (taking up 24 hours) to include a case study on reasoning in Ontologies (to be given by Graham Deane – 4 hours).
The notes here are for the 2013/2014 session (Graham’s notes will be issued separately).
My 24 hours will cover:
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 proving
These (older) notes amplify the lecture notes, but are not required reading for examination purposes
- Herbrand’s Theorem and Resolution
- Controlling Resolution
- Notes on Connection Graph Procedure
- Notes on Clausal Tableaux
- Notes on Paramodulation
Lecture notes Spring 2014:
- Davis Putnam
- Some Background
- Appendix1: Slides 3 to 6 proofs
- Controlling Resolution
- Hyper Resolution and Otter
- Semantic Tableaux
- Clausal Tableaux
- Various Clasual Tableaux Refinements
- Appendix 2: Some Miscellaneous notes on Tableaux
- Equality and Tableaux
- Ordering Rewrite Rules
- Knuth Bendix Completion
- Knuth Bendix Extras
Please see CATE for problem sheets and answers.
The Pandora and Raptor Teaching Tools in Logic
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).
- Alternatively, you can find Pandora at New Pandora download page See also Pandora: A Reasoning Toolbox using Natural Deduction Style K. Broda, J. Ma, G. Sinadurai and A.J. Summers in Logic Journal of the IGPL 15:293-304, 2007