Visual Theorem Proving with the Incredible Proof Machine
Visual Theorem Proving with the Incredible Proof Machine
复制标题
用令人难以置信的证明机证明视觉定理
DOI：
10.1007/978-3-319-43144-4_8
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Joachim Breitner
中科院分区：
文献类型：
--
作者：
Joachim Breitner
不可思议的证明机是一个简单而有趣的程序来进行正式的证明。它采用了一种基于端口图的新颖、直观的证明表示，它类似于自然演绎，但比自然演绎更自然。特别地，我们描述了一种隐式地确定局部假设和变量范围的方法。我们的实际课堂经验支持这些说法。
The Incredible Proof Machine is an easy and fun to use program to conduct formal proofs. It employs a novel, intuitive proof representation based on port graphs, which is akin to, but even more natural than, natural deduction. In particular, we describe a way to determine the scope of local assumptions and variables implicitly. Our practical classroom experience backs these claims.