An Interactive Derivation Viewer

Steven Trac, Yury Puzis, Geoffrey Sutcliffe

Research output: Contribution to journalArticle

19 Citations (Scopus)

Abstract

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
Volume174
Issue number2
DOIs
StatePublished - May 15 2007

Fingerprint

Web browsers
Interfaces (computer)
Rendering
Lemma

Keywords

  • Derivation viewer
  • Proof synopsis

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

An Interactive Derivation Viewer. / Trac, Steven; Puzis, Yury; Sutcliffe, Geoffrey.

In: Electronic Notes in Theoretical Computer Science, Vol. 174, No. 2, 15.05.2007, p. 109-123.

Research output: Contribution to journalArticle

Trac, Steven ; Puzis, Yury ; Sutcliffe, Geoffrey. / An Interactive Derivation Viewer. In: Electronic Notes in Theoretical Computer Science. 2007 ; Vol. 174, No. 2. pp. 109-123.
@article{2c4e05f9dda14a3aa374d47c2fd28160,
title = "An Interactive Derivation Viewer",
abstract = "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.",
keywords = "Derivation viewer, Proof synopsis",
author = "Steven Trac and Yury Puzis and Geoffrey Sutcliffe",
year = "2007",
month = "5",
day = "15",
doi = "10.1016/j.entcs.2006.09.025",
language = "English (US)",
volume = "174",
pages = "109--123",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "2",

}

TY - JOUR

T1 - An Interactive Derivation Viewer

AU - Trac, Steven

AU - Puzis, Yury

AU - Sutcliffe, Geoffrey

PY - 2007/5/15

Y1 - 2007/5/15

N2 - 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.

AB - 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.

KW - Derivation viewer

KW - Proof synopsis

UR - http://www.scopus.com/inward/record.url?scp=34247860714&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=34247860714&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2006.09.025

DO - 10.1016/j.entcs.2006.09.025

M3 - Article

AN - SCOPUS:34247860714

VL - 174

SP - 109

EP - 123

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 2

ER -