PANDORA - a Natural Deduction Proof Tool
Pandora is a Natural Deduction boxproof tool which was developed by
students in previous projects. It consists of two parts; one is an editor
written in Tcl/Tk and the other is a checker/debugger written in Prolog.
They communicate via a simple interface. The tool is used in teaching first
There are several projects available to work on this tool:
This project could suit several persons each working on different aspects
of the tool.
- Extend the proof editor in one or more of several different directions:
For example, possibilities include:
- to change the syntax to include typed quantifiers and to reason
- to improve the unification and editing facilities;
- to incorporate reasoning within mathematical induction and rewrite
- Port the editor to a PC.
- Include other logics, for example propositional modal logic or
- Automate some of the steps.