System BV of the Calculus of Structures in Tom

You may try to prove structures like:

This applet implemements the ideas in the following paper.

Implementing Deep Inference in TOM
Ozan Kahramanogullari, Pierre-Etienne Moreau and Antoine Reilles
Presented at the Structures and Deduction Workshop 2005, SD'05, ICALP'05 Satellite, Lisbon, Portugal, July 2005
Download: PDF file
PS file
Bib TeX entry