Teaching

Current Teaching

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

Hand Outs from Lecture (2013)

Getting started with Otter

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

Background notes:

These (older) notes amplify the lecture notes, but are not required reading for examination purposes

 

Lecture notes Spring 2014:

Problem Sheets

Please see CATE for problem sheets and answers.

Back to top

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).