发帖
雷达卡
摘要翻译：
当数学家提出证明时，他们通常根据他们的教学目标和他们的对象的（假定的）知识来调整他们的解释。相比之下，现代的自动定理证明者通常在固定的细节级别（也称为粒度）上提出证明。通常，这些演示既不是有意的，也不适合人类使用。因此，一个挑战是开发符合普通数学实践的用户和目标自适应的证明表示技术。提出了一种灵活自适应的证明表示方法，利用机器学习技术提取特定粒度证明实例的模型，并利用该模型在适当的粒度水平上自动生成进一步的证明。
---
英文标题：
《Granularity-Adaptive Proof Presentation》
---
作者：
Marvin Schiller and Christoph Benzmueller
---
最新提交年份：
2009
---
分类信息：
一级分类：Computer Science 计算机科学
二级分类：Artificial Intelligence 人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--
---
英文摘要：
When mathematicians present proofs they usually adapt their explanations to their didactic goals and to the (assumed) knowledge of their addressees. Modern automated theorem provers, in contrast, present proofs usually at a fixed level of detail (also called granularity). Often these presentations are neither intended nor suitable for human use. A challenge therefore is to develop user- and goal-adaptive proof presentation techniques that obey common mathematical practice. We present a flexible and adaptive approach to proof presentation that exploits machine learning techniques to extract a model of the specific granularity of proof examples and employs this model for the automated generation of further proofs at an adapted level of granularity.
---
PDF链接：
https://arxiv.org/pdf/0903.0314
京公网安备 11010802022788号
