Simplifying the axiomatization for ordered affine geometry via a theorem prover

被引：0
|
作者：
Li, Dafa [1 ]
机构：
[1] Tsinghua Univ, Dept Math Sci, Beijing 100084, Peoples R China
来源：
JOURNAL OF GEOMETRY | 2023年 / 114卷 / 02期
关键词：
Ordered affine geometry; Axiomatization; Automated theorem proving; Intuitionistic logic;
D O I：
10.1007/s00022-023-00671-9
中图分类号：
O1 [数学];
学科分类号：
0701 ; 070101 ;
摘要：
Jan von Plato proposed in 1998 an intuitionist axiomatization of ordered affine geometry consisting of 22 axioms. It is shown that axiom I.7, which is equivalent to a conjunction of four statements, two of which are redundant, can be replaced with a simpler axiom, which is von Plato's Theorem 3.10.
引用
收藏
页数：6
相关论文
共 46 条
12345