Enhancement of MIZAR Texts with Transitivity Property of Predicates

被引：4
|
作者：
Kornilowicz, Artur [1 ]
机构：
[1] Univ Bialystok, Inst Informat, K Ciolkowskiego 1M, PL-15245 Bialystok, Poland
来源：
Intelligent Computer Mathematics | 2016年 / 9791卷
关键词：
D O I：
10.1007/978-3-319-42547-4_12
中图分类号：
TP39 [计算机的应用];
学科分类号：
081203 ; 0835 ;
摘要：
A typical proof step in mathematical reasoning consists of two parts - a formula to be proven and a list of references used to justify the formula. In addition, computer proof-assistants can use specialized procedures and algorithms to strengthen their computational power to verify the correctness of reasonings. The Mizar system supports several mechanisms to increase automation of some reasoning steps. One of them is registration of chosen properties of predicates and functors when they are defined. We propose strengthening of the Mizar system by processing another common property used in mathematics - transitivity.
引用
收藏
页码：157 / 162
页数：6
相关论文
共 50 条
12345