论文标题

通过引理流程图的基于代理的证明设计

Agent-Based Proof Design via Lemma Flow Diagram

论文作者

Kwon, Keehang, Kang, Daeseong

论文摘要

我们讨论了一种基于代理的证明设计和实现方法,我们称之为{\ it lemma流程图}(LFD)。这种方法基于具有$共享$削减的多通用规则。这种方法是模块化的,易于使用,阅读和自动化。因此,我们认为LFD是在数学教育中流行的“流动证明”的吸引人替代方案。提供了一些示例。

We discuss an agent-based approach to proof design and implementation, which we call {\it Lemma Flow Diagram} (LFD). This approach is based on the multicut rule with $shared$ cuts. This approach is modular and easy to use, read and automate. Thus, we consider LFD an appealing alternative to `flow proof' which is popular in mathematical education. Some examples are provided.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源