**Idea:**
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
year students.
There are several projects available to work on this 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 with them;
- to improve the unification and editing facilities;
- to incorporate reasoning within mathematical induction and rewrite proofs;

- Port the editor to a PC.
- Include other logics, for example propositional modal logic or linear/relevance logic.
- Automate some of the steps.