自动定理证明兴衰纪(下)

• 作者: 尼克
• 来源期刊: 中国计算机学会通讯
• 关键词: 自动定理证明 人工智能 逻辑学 数学
• 年，卷（期）: 2016,（8）
• 所属期刊栏目: 专栏
• 页码范围: 52-56
• 页数: 5页
• 语种: 中文

摘要

符号派的内部矛盾 大多数定理证明器都使用反证法,即将待证命题的否命题输入系统,得出矛盾(即空子句),从而证明原命题.定理证明一般只能回答“是”或“否”,但有时我们需要证明结果能提供更多信息.例如,假设我们面对一个定理证明系统,想知道它是否包含这样的事实“谁是玛丽(Mary)的丈夫?”.那么我们可以问:～Husband(x,Mary).

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	尼克		2	0	0.0	0.0