An Interactive Derivation Viewer

Steven Trac, Yury Puzis, Geoff Sutcliffe

Research output: Contribution to journalArticlepeer-review

20 Scopus citations


This work describes the Interactive Derivation Viewer (IDV) tool for graphical rendering of derivations that are written in the TPTP language. IDV provides an interactive interface that allows the user to quickly view various features of the derivation. A particularly novel feature of IDV is its ability to provide a synopsis of a derivation by identifying interesting lemmas within a derivation, and hiding less interesting intermediate formulae. IDV is deployed online as part of the SystemOnTPTP interface, thus providing ready access via any web browser.

Original languageEnglish (US)
Pages (from-to)109-123
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
Issue number2
StatePublished - May 15 2007


  • Derivation viewer
  • Proof synopsis

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'An Interactive Derivation Viewer'. Together they form a unique fingerprint.

Cite this