Instance-Based Theorem Proving with Semantics and Equality
Instance-Based Theorem Proving with Semantics and Equality
批准号:
9972118
负责人:
David Plaisted
金额:
$24.51万
依托单位国家:
美国
项目类别:
Standard Grant
财政年份:
1999
资助国家:
美国
项目状态:
已结题
起止时间:
1999-08-01 至 2003-07-31
中文摘要
有序语义超链接策略(OSHL)将命题效率、语义和等价性结合在一个集成的一阶逻辑自动定理证明器中。语义是指符号的意义,命题效率是指对需要进行重大案例分析的问题的效率。现有的证明者很少利用语义,而且大多数都不是命题有效的。目前的PROLOG实施将按照最近一篇关于这一主题的论文所建议的方式进行扩展。为了提高速度,方案中还将重新实现证明器。此外,还将实现一个结合了等价性、统一性和命题效率但没有语义的证明器,因为语义可能不总是可用的。在一类重大问题上,这些组合应该会比几乎所有其他证明者表现得更好。还将寻求能够在数百万个输入子句集合上有效证明定理的技术。
英文摘要
The ordered semantic hyper-linking strategy (OSHL) combines propositional efficiency, semantics, and equality in one integrated automatic theorem prover for first-order logic. Semantics refers to the meaning of symbols, and propositional efficiency refers to efficiency on problems requiring significant case analysis. Few existing provers utilize semantics, and most are not propositionally efficient. The current Prolog implementation will be extended in ways that were suggested by a recent paper on the topic. The prover will also be re-implemented in Scheme for greater speed. In addition, a prover combining equality, unification, and propositional efficiency but no semantics will be implemented, because semantics may not always be available. These combinations should outperform almost all other provers on a significant class of problems. Techniques capable of effective theorem proving on sets of millions of input clauses will also be sought.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
Instance-Based Theorem Proving with Semantics and Equality
-
批准号:9627316
-
项目类别:Standard Grant
-
资助金额:$8.92万
-
财政年份:1996
-
负责人:David Plaisted
-
依托单位:
Hyper-Linking with Equality and Semantics
-
批准号:9108904
-
项目类别:Continuing Grant
-
资助金额:$19.28万
-
财政年份:1992
-
负责人:David Plaisted
-
依托单位:
Research in Term Rewriting Systems and Automated Deduction,
-
批准号:8802282
-
项目类别:Continuing Grant
-
资助金额:$16.08万
-
财政年份:1988
-
负责人:David Plaisted
-
依托单位:
Research in Automated Deduction and Term Rewriting Systems
-
批准号:8516243
-
项目类别:Standard Grant
-
资助金额:$19.04万
-
财政年份:1986
-
负责人:David Plaisted
-
依托单位:
Term - Rewriting Systems
-
批准号:7904897
-
项目类别:Standard Grant
-
资助金额:$22.43万
-
财政年份:1979
-
负责人:David Plaisted
-
依托单位:
国内基金
海外基金
登录
查看更多内容
Data-driven Recommendation System Construction of an Online Medical Platform Based on the Fusion of Information
-
批准号:--
-
项目类别:外国青年学者研究基金项目
-
资助金额:--
-
批准年份:2024
-
负责人:江洋子
-
依托单位:
Incentive and governance schenism study of corporate green washing behavior in China: Based on an integiated view of econfiguration of environmental authority and decoupling logic
-
批准号:--
-
项目类别:外国学者研究基金项目
-
资助金额:--
-
批准年份:2024
-
负责人:YU BYUNGJUN
-
依托单位:
Exploring the Intrinsic Mechanisms of CEO Turnover and Market Reaction: An Explanation Based on Information Asymmetry
-
批准号:W2433169
-
项目类别:外国学者研究基金项目
-
资助金额:--
-
批准年份:2024
-
负责人:HAOFEI ZHANG
-
依托单位:
A study on prototype flexible multifunctional graphene foam-based sensing grid (柔性多功能石墨烯泡沫传感网格原型研究)
-
批准号:--
-
项目类别:--
-
资助金额:20万元
-
批准年份:2020
-
负责人:SAGAR RIZWAN UR REHMAN
-
依托单位:
基于tag-based单细胞转录组测序解析造血干细胞发育的可变剪接
-
批准号:81900115
-
项目类别:青年科学基金项目
-
资助金额:21.0万元
-
批准年份:2019
-
负责人:李宗城
-
依托单位:
应用Agent-Based-Model研究围术期单剂量地塞米松对手术切口愈合的影响及机制
-
批准号:81771933
-
项目类别:面上项目
-
资助金额:50.0万元
-
批准年份:2017
-
负责人:周全红
-
依托单位:
Reality-based Interaction用户界面模型和评估方法研究
-
批准号:61170182
-
项目类别:面上项目
-
资助金额:57.0万元
-
批准年份:2011
-
负责人:田丰
-
依托单位:
Multistage,haplotype and functional tests-based FCAR 基因和IgA肾病相关关系研究
-
批准号:30771013
-
项目类别:面上项目
-
资助金额:30.0万元
-
批准年份:2007
-
负责人:王一鸣
-
依托单位:
差异蛋白质组技术结合Array-based CGH 寻找骨肉瘤分子标志物
-
批准号:30470665
-
项目类别:面上项目
-
资助金额:8.0万元
-
批准年份:2004
-
负责人:李扬
-
依托单位:
GaN-based稀磁半导体材料与自旋电子共振隧穿器件的研究
-
批准号:60376005
-
项目类别:面上项目
-
资助金额:20.0万元
-
批准年份:2003
-
负责人:张国义
-
依托单位: