Instance-Based Theorem Proving with Semantics and Equality
基于实例的定理证明语义和等式
基本信息
- 批准号:9972118
- 负责人:
- 金额:$ 24.51万
- 依托单位:
- 依托单位国家:美国
- 项目类别:Standard Grant
- 财政年份:1999
- 资助国家:美国
- 起止时间:1999-08-01 至 2003-07-31
- 项目状态:已结题
- 来源:
- 关键词:
项目摘要
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.
有序语义超链接策略(OSHL)将命题效率、语义和等价性结合在一个集成的一阶逻辑自动定理证明器中。语义是指符号的意义,命题效率是指对需要进行重大案例分析的问题的效率。现有的证明者很少利用语义,而且大多数都不是命题有效的。目前的PROLOG实施将按照最近一篇关于这一主题的论文所建议的方式进行扩展。为了提高速度,方案中还将重新实现证明器。此外,还将实现一个结合了等价性、统一性和命题效率但没有语义的证明器,因为语义可能不总是可用的。在一类重大问题上,这些组合应该会比几乎所有其他证明者表现得更好。还将寻求能够在数百万个输入子句集合上有效证明定理的技术。
项目成果
期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
数据更新时间:{{ journalArticles.updateTime }}
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
数据更新时间:{{ journalArticles.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ monograph.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ sciAawards.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ conferencePapers.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ patent.updateTime }}
David Plaisted其他文献
David Plaisted的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('David Plaisted', 18)}}的其他基金
Instance-Based Theorem Proving with Semantics and Equality
基于实例的定理证明语义和等式
- 批准号:
9627316 - 财政年份:1996
- 资助金额:
$ 24.51万 - 项目类别:
Standard Grant
Hyper-Linking with Equality and Semantics
具有平等性和语义的超链接
- 批准号:
9108904 - 财政年份:1992
- 资助金额:
$ 24.51万 - 项目类别:
Continuing Grant
Research in Term Rewriting Systems and Automated Deduction,
术语重写系统和自动演绎研究,
- 批准号:
8802282 - 财政年份:1988
- 资助金额:
$ 24.51万 - 项目类别:
Continuing Grant
Research in Automated Deduction and Term Rewriting Systems
自动演绎和术语重写系统的研究
- 批准号:
8516243 - 财政年份:1986
- 资助金额:
$ 24.51万 - 项目类别:
Standard Grant
相似国自然基金
Data-driven Recommendation System Construction of an Online Medical Platform Based on the Fusion of Information
- 批准号:
- 批准年份:2024
- 资助金额:万元
- 项目类别:外国青年学者研究基金项目
Exploring the Intrinsic Mechanisms of CEO Turnover and Market Reaction: An Explanation Based on Information Asymmetry
- 批准号:W2433169
- 批准年份: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
- 资助金额:万元
- 项目类别:外国学者研究基金项目
A study on prototype flexible multifunctional graphene foam-based sensing grid (柔性多功能石墨烯泡沫传感网格原型研究)
- 批准号:
- 批准年份:2020
- 资助金额:20 万元
- 项目类别:
基于tag-based单细胞转录组测序解析造血干细胞发育的可变剪接
- 批准号:81900115
- 批准年份:2019
- 资助金额:21.0 万元
- 项目类别:青年科学基金项目
应用Agent-Based-Model研究围术期单剂量地塞米松对手术切口愈合的影响及机制
- 批准号:81771933
- 批准年份:2017
- 资助金额:50.0 万元
- 项目类别:面上项目
Reality-based Interaction用户界面模型和评估方法研究
- 批准号:61170182
- 批准年份:2011
- 资助金额:57.0 万元
- 项目类别:面上项目
Multistage,haplotype and functional tests-based FCAR 基因和IgA肾病相关关系研究
- 批准号:30771013
- 批准年份:2007
- 资助金额:30.0 万元
- 项目类别:面上项目
差异蛋白质组技术结合Array-based CGH 寻找骨肉瘤分子标志物
- 批准号:30470665
- 批准年份:2004
- 资助金额:8.0 万元
- 项目类别:面上项目
GaN-based稀磁半导体材料与自旋电子共振隧穿器件的研究
- 批准号:60376005
- 批准年份:2003
- 资助金额:20.0 万元
- 项目类别:面上项目
相似海外基金
Development of Nanoscale Viscoelasticity Measurement Method Based on Fluctuation-Dissipation Theorem
基于涨落耗散定理的纳米级粘弹性测量方法的发展
- 批准号:
23H02021 - 财政年份:2023
- 资助金额:
$ 24.51万 - 项目类别:
Grant-in-Aid for Scientific Research (B)
Non-linear fluctuating hydrodynamics based on fluctuation theorem
基于涨落定理的非线性脉动流体动力学
- 批准号:
19K21881 - 财政年份:2019
- 资助金额:
$ 24.51万 - 项目类别:
Grant-in-Aid for Challenging Research (Exploratory)
Study on sound space sensing based on an extended spatial sampling theorem
基于扩展空间采样定理的声音空间感知研究
- 批准号:
19K12026 - 财政年份:2019
- 资助金额:
$ 24.51万 - 项目类别:
Grant-in-Aid for Scientific Research (C)
Defect inspection method based on Cauchy's integral theorem using a circular differential coherent illumination
基于柯西积分定理的圆形差分相干照明缺陷检测方法
- 批准号:
18K04172 - 财政年份:2018
- 资助金额:
$ 24.51万 - 项目类别:
Grant-in-Aid for Scientific Research (C)
An exploratory study toward a foundation of nonequilibrium statistical mechanics based on the fluctuation theorem
基于涨落定理的非平衡统计力学基础的探索性研究
- 批准号:
17K18737 - 财政年份:2017
- 资助金额:
$ 24.51万 - 项目类别:
Grant-in-Aid for Challenging Research (Exploratory)
Ground motion prediction method for arbitrary seismic source based on the reciprocity theorem of Green's function and ground motion record
基于格林函数互易定理和地震动记录的任意震源地震动预测方法
- 批准号:
25889032 - 财政年份:2013
- 资助金额:
$ 24.51万 - 项目类别:
Grant-in-Aid for Research Activity Start-up
Free boundary problems for flows with phase transitions consistent with thermodynamics based on maximal regularity theorem
基于最大正则定理的符合热力学的相变流动自由边界问题
- 批准号:
24340025 - 财政年份:2012
- 资助金额:
$ 24.51万 - 项目类别:
Grant-in-Aid for Scientific Research (B)
Unified viewpoint for hypergeometric functions and the pentagonal number theorem based on representation theory
基于表示论的超几何函数与五边形数定理的统一观点
- 批准号:
23654050 - 财政年份:2011
- 资助金额:
$ 24.51万 - 项目类别:
Grant-in-Aid for Challenging Exploratory Research
An automatic unpacking method for computer virus effective in the virus filter based on Bayesian theorem
基于贝叶斯定理的有效病毒过滤的计算机病毒自动脱壳方法
- 批准号:
23500074 - 财政年份:2011
- 资助金额:
$ 24.51万 - 项目类别:
Grant-in-Aid for Scientific Research (C)
Developments of new linear solvers based on the induced dimension reduction theorem
基于诱导降维定理的新型线性求解器的开发
- 批准号:
22560067 - 财政年份:2010
- 资助金额:
$ 24.51万 - 项目类别:
Grant-in-Aid for Scientific Research (C)