displaying proof trees

[Larry Moss]

I have a Sage program that generates 'proof trees', running on the cloud.   

I generate trees,  nested lists like

[U, [S, T, V, Barbara], W, Darii]

The last item in each subtree is a label that requires special handling.

I'd like to do two things with these trees.

(1)  I'd like to display them on the screen as something like

    

        T       V

    ------------------- Barbara

             S                                        W

    --------------------------------------------- Darii

                                   U

                                   

                                   

 (2) I'd also like to recursively translate translate to a LaTeX expression.

 For example, using proof.sty, I would want

 

 \infer[Darii]{U}{\infer[Barbara]{S}{T & V} & W}                          

 

 Any ideas on how I can do either of these?

 

 For now, I 'linearize' the tree to something like

 

 1  T  Assumption

 2  V Assumption

 3 S  Barbara 1, 2

 4 W Assumption

 5 U  Darii 3, 4