Coq & ProofWeb
在ProofWeb的主页http://prover.cs.ru.nl点击按钮
，然后在Select a saved file to load:中选择
tarski-hg.v，然后在下面的下拉框中选择
Coq，点
，就可以看到Tarski’s Fixed Point Theorem的形式化证明过程，这个证明过程可以作为Coq和ProofWeb的一个不错的demo。
荒唐的世界
逻辑引擎
近期评论
- 荒唐 发表在《道德》
- blackhole 发表在《道德》
- 荒唐 发表在《关于价值观》
- 荒唐 发表在《连转带评：纽科姆悖论》
- 三思正和 发表在《连转带评：纽科姆悖论》
- 三思正和 发表在《关于价值观》
- 荒唐 发表在《黑洞——要么无法形成，要么不会蒸发》
- 三思正和 发表在《黑洞——要么无法形成，要么不会蒸发》
- 荒唐 发表在《博士政治课的大作业》
- crazyseti 发表在《博士政治课的大作业》
- 荒唐 发表在《图灵机vs数学家——图灵机计算能力的分析》
- scc 发表在《图灵机vs数学家——图灵机计算能力的分析》
- Maverick 发表在《黑洞——要么无法形成，要么不会蒸发》
- 荒唐 发表在《说明》
- 荒唐 发表在《说明》
- Daniel 发表在《几种
插件比较》
近期文章
- 什么是病？
- 抬杠专业户是怎样炼成的～～
- 我对热力学第二定律的统计解释
- Benford’s Law
- 转载，数学反例
- 方舟子的信仰和价值偏见
- 经典多体问题的非碰撞奇点解简介
- 连转带评：纽科姆悖论
- 道德
- 关于价值观
- 概念的含义
- 对量子力学之中不确定关系的解释
- 几十年来歌功颂德影视剧的演化
- 梦的解析
- 恐怖电影中的元素
- [ZZ]“瑞典模式”再次成为样板
- 高福利体现了人权么？
- 关于政治坐标中的左右
- 关于普世价值的种种论调
- 手语电话
- 博士政治课的大作业
- test for Quick
- [ZZ]火车进入山洞
- 给新程序员的一些建议
- 记者因文章被停职
- [ZZ]技术左右天下大势
- [ZZ]计算机围棋科幻小说——《墨绿》
- 简单回合制游戏
- 关于下岗和圈地的讨论
- 传说……
- 理论的可检验性和有效性。
- 论证『科学也是一种信仰』的若干伎俩
- 私有产权神圣不可侵犯只是廉价的谎言。
- The knowledge that I don’t want to learn.
- 整体大于其组成部分之和
- Not a big deal
- 吹牛逼和爱国主义
- 左右
- 浪漫地讲道理？
- 关于爱心捐助
- [ZZ]选民的大脑想要什么——同人于野
- 谚语：挡人财路，如同杀人父母
- Coq & ProofWeb
- Zorn’s Lemma
- 感官感受能欺骗我们么？
- 恰当的问题
- 黑洞——要么无法形成，要么不会蒸发
- 关于无穷这个词的意义
- Reinvent wheels, my quick sort implementation, just for fun
- Finding all paths from source to destination
