利用性质省略导出MIZAR数学库中证明的隐式假设
Eliciting implicit assumptions of proofs in the MIZAR Mathematical Library by property omission
摘要：
当使用交互式定理证明器进行形式化证明时，经常会发生关于数学概念的额外背景知识（声明性或过程性）被采用而形式化器没有显式地调用它，以帮助形式化器专注于证明的相关细节。在产生和研究形式化的数学论证的背景下，这种机制显然是有价值的。但我们可能并不总是希望压制背景知识。为了某些目的，尽可能精确地知道在形式证明中隐含地使用了什么背景知识是很重要的。在本文中，我们描述了在MIZAR数学库的正式数学证明上进行的一个实验，以引出一类隐含使用的背景知识：函数和关系的性质（例如，交换性、不对称性等）。
英文摘要：
When formalizing proofs with interactive theorem provers, it often happens that extra background knowledge (declarative or procedural) about mathematical concepts is employed without the formalizer explicitly invoking it, to help the formalizer focus on the relevant details of the proof. In the contexts of producing and studying a formalized mathematical argument, such mechanisms are clearly valuable. But we may not always wish to suppress background knowledge. For certain purposes, it is important to know, as far as possible, precisely what background knowledge was implicitly employed in a formal proof. In this note we describe an experiment conducted on the MIZAR Mathematical Library of formal mathematical proofs to elicit one such class of implicitly employed background knowledge: properties of functions and relations (e.g., commutativity, asymmetry, etc.).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
