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