System BV of the Calculus of Structures in Tom

You may try to prove structures like:
[a,b,(-a,-c),(-b,c)]
[-a,([c,-c],[-b,(a,b)])]
[[(a,b),-a,-b],[(c,[(a,b),-a]),-b,-c]]


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