The Tinker tool for graphical tactic development
The Tinker tool for graphical tactic development
复制标题
用于图形战术开发的 Tinker 工具
DOI：
10.1007/s10009-017-0452-7
复制
发表时间：
2017
影响因子：
1.5
通讯作者：
Grov G
中科院分区：
文献类型：
--
作者：
Grov G
PSGraph（Grov等人，LPAR. Springer，柏林，第324-339页，2013）是一种图形语言，用于支持交互式定理证明器的证明策略的开发和维护。通过使用标记的层次图，这种形式化改进了传统战术语言中的分析和维护。对PSGraph的工具支持由Tinker实现（Grov等人，在2014年的《网络安全与安全》，第167卷）。Open Publishing Association，伦敦，第23-34页，2014年; Lin et al. in Tools and algorithms for the construction and analysis of systems. Springer，柏林，第573-579页，2016年）：一个独立于定理证明器的系统，它连接到几个不同的证明器，具有图形用户界面，包括图形化开发和调试证明策略的新功能。在本文中，我们提供了一个详细的和正式的PSGraph帐户，并显示定理证明独立性是如何实现的修补匠。然后，我们通过使用语言和工具开发几种证明模式来展示PSGraph和Tinker的实际使用。
PSGraph(Grov et al. in LPAR. Springer, Berlin, pp 324–339, 2013) is a graphical language to support the development and maintenance of proof tactics for interactive theorem provers. By using labelled hierarchical graphs this formalisation improves upon analysis and maintenance found in traditional tactic languages. Tool support for PSGraph is achieved byTinker(Grov et al. in UITP 2014, ENTCS, vol 167. Open Publishing Association, London, pp 23–34, 2014; Lin et al. in Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 573–579, 2016): a theorem prover-independent system, which is connected to several different provers, with a graphical user interface including novel features to develop and debug proof tactics graphically. In this paper we provide a detailed and formal account of PSGraph and show how theorem prover independence is achieved by Tinker. We then show practical use of PSGraph and Tinker by developing several proof patterns using the language and tool.
登录
查看更多内容
推理科学（扩展摘要）
DOI：
--
发表时间：
1998
期刊：
International Conference on Theorem Proving with Analytic Tableaux and Related Methods
影响因子：
--
作者：
A. Bundy
通讯作者：
A. Bundy
DOI：
--
发表时间：
2010
期刊：
影响因子：
--
作者：
Karol Pąk
通讯作者：
Karol Pąk
Rippling - 数学推理的元级指导
DOI：
10.1017/cbo9780511543326
发表时间：
2005
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
A. Bundy;D. Basin;D. Hutter;Andrew Ireland
通讯作者：
Andrew Ireland
ProveEasy：帮助人们学习证明
DOI：
--
发表时间：
2000
期刊：
Computing: The Australasian Theory Symposium
影响因子：
--
作者：
R. Burstall
通讯作者：
R. Burstall
Jape：纸上校样动画计算器
DOI：
10.1007/3-540-63104-6_41
发表时间：
1997
期刊：
Proceedings of the 33rd Annual ACM Conference on Human Factors in Computing Systems
影响因子：
--
作者：
R. Bornat;B. Sufrin
通讯作者：
B. Sufrin