首页> 外文期刊>urnal of Symbolic Computation >Computer proofs about finite and regular sets: the unifying concept of subvariance
【24h】

Computer proofs about finite and regular sets: the unifying concept of subvariance

机译:关于有限和正则集的计算机证明:子方差的统一概念

获取原文
获取原文并翻译 | 示例
           

摘要

The work described here is a part of ongoing efforts to construct a set-theoretic framework that is convenient for automated reasoning in mathematics within first order logic. The specific topic in focus here is the theory of invariant and subvariant sets, which permits the development of a unified theory of regular and finite sets. Appendices are included listing theorems involving the axiom of regularity, the classes REGULAR and FINITE of regular sets and finite sets, respectively, as well as general theorems about invariant and subvariant subsets, all proved using McCune's automated reasoning program Otter.
机译:这里描述的工作是构建集合理论框架的正在进行的工作的一部分,该集合理论框架便于在一阶逻辑内进行数学中的自动推理。这里关注的特定主题是不变和子变集的理论,它允许发展正则和有限集的统一理论。附录中列出了涉及正则性公理的定理,分别为正则集和有限集的REGULAR和FINITE类以及关于不变和子变量子集的一般定理,所有定理均使用McCune的自动推理程序Otter证明。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号