Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


Natural Deduction Calculus for Temporal Logic and its Automation

  • Speaker:   Dr  Alexander Bolotov  (University of Westminster)
  • Host:   Ian Pratt-Hartmann
  • 10th October 2007 at 14:15 in Lecture Theatre 1.4, Kilburn Building
Joint work with Oleg Grigoriev and Vasilyi Shangin (Moscow State University) and Artie Basukoski and Gaurav Gupta (University of Westminster)

Natural deduction (ND) systems that are due to Jaskowski, Fitch and Quine are interesting as they represent a `natural' way of reasoning. Natural Deduction has been primarily studied within the framework of philosophical logic, being widely used in teaching, but for a while ignored in the area of automated reasoning. For the last few decades, however, ND systems have been considered as appropriate for an algorithmic representation.

We present the results of a long term project on developing ND constructions for various classical and non-classical logics and corresponding generic proof searching techniques. The main principles of these proof search procedures will be explained on the example of classical logic followed up by the extension to propositional temporal logic. We will accompany the presentation by a demonstration of an ND theorem prover. An earlier version of the implementation for classical propositional logic is available on-line at and the most recent implementation which can also tackle some core examples (such as Pigeon Hole principle) and temporal reasoning (still under development) is available at
▲ Up to the top