杭州电子科技大学图书馆书目检索系统

Online Public Access Catalogue

题名/责任者:

公理化集合论机器证明系统/郁文生, 孙天宇, 付尧顺著

出版发行项:

北京:科学出版社,2020

ISBN及定价:

978-7-03-064039-0 精装/CNY128.00

载体形态项:

xiii, 293页, [1] 页图版:彩图;25cm

丛编项:

数学机械化丛书;13

个人责任者:

郁文生 著

个人责任者:

孙天宇 著

个人责任者:

付尧顺 著

学科主题:

集论公理系统-机器证明

中图法分类号:

O144-39

书目附注:

有书目 (第284-289页) 和索引

提要文摘附注:

本书利用交互式定理证明工具Coq，实现Morse-Kelley公理化集合论形式化系统，包括对该体系中8个公理(含选择公理)和1个公理图示以及全部181条定义或定理的Coq描述，其中构造了序数和基数，定义了非负整数，把Peano公设当作定理，可以迅速而自然地给出一个数学基础，摆脱了明显的悖论。

豆瓣简介：