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实现将以最近一篇关于该主题的论文所建议的方式进行扩展。 为了更快的速度,还将在Scheme中重新实现该校准器。 此外,将实现一个结合了等式、统一和命题效率但没有语义的证明器,因为语义可能并不总是可用的。 这些组合应该优于几乎所有其他证明的一类重要的问题。 技术能够有效的定理证明集的数百万输入条款也将寻求。
英文摘要
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
-
负责人:张国义
-
依托单位: