Traf: A Graphical Proof Tree Viewer Cooperating with Coq Through Proof General

Traf is a graphical proof tree viewer that cooperates with the Coq proof assistant and is controlled through Proof General. Among other proof tree viewers and tools for browsing proof scripts, Traf is well suited for daily proving of Coq problems as it is easy to use, non-disturbing, and helpful. Proof trees dynamically updated by Traf during interactive sessions with Proof General are informative and as readable as Gentzen-style natural deduction proofs. Traf facilitates browsing and investigating tactic-based proof scripts, which are often burdensome to read. Traf can also be used for typesetting proof trees with Open image in new window . The current version of Traf was developed as an extension to the Prooftree proof tree viewer and makes use of many of its facilities. Traf provides functionalities that are useful to both novice Coq users and experienced Proof General users.