An Interactive Derivation Viewer
An Interactive Derivation Viewer
复制标题
交互式推导查看器
DOI：
10.1016/j.entcs.2006.09.025
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
G. Sutcliffe
中科院分区：
文献类型：
--
作者：
Steven Trac;Yury Puzis;G. Sutcliffe
这项工作介绍了交互式派生查看器（IDV）工具的图形化呈现的派生，写在TPTP语言。IDV提供了一个交互式界面，允许用户快速查看派生的各种功能。IDV的一个特别新颖的功能是它能够通过识别推导中有趣的引理来提供推导的概要，并隐藏不太有趣的中间公式。IDV作为SystemOnTPTP接口的一部分在线部署，因此可以通过任何Web浏览器随时访问。
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.