Collaborative Research on Semantic Unification and its Applications

语义统一及其应用的协作研究

基本信息

批准号：
0098114
负责人：
Deepak Kapur
金额：
$ 13.71万
依托单位：
University of New Mexico
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2001
资助国家：
美国
起止时间：
2001-08-15 至 2005-07-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=0098114&HistoricalAwards=false
关键词：
Collaborative Research Semantic Unification its

项目摘要

Proposal #0098114Kupar, DeepakUniversity of MexicoSemantic unification has been effectively employed in many subfields of logic, computer science, artificial intelligence and cognitive science, with its most popular use being in resolution, logic programming languages such as Prolog, and the type inference mechanism in the programming language ML. Semantic unification (associative-commutative unification) played a pivotal role in settling open questions in mathematics (e.g. Robbins' conjecture about boolean algebra in 1996 by McCune using the theorem prover EQP). Recently, semantic unification has been found useful also in cryptographic analysis, knowledge representation and distributed computing.This project will be a continuation of research on the theory of semantic unification as well as the design, development and implementation of semantic unification algorithms. This research will be motivated by new applications of semantic unification in cryptographic protocol analysis in conjunction with Catherine Meadows' work on the NRL (Naval Research Laboratory) Protocol Analyzer, in knowledge representation and description logics, induction theorem proving, and process algebra.The new unification algorithms will be first developed and experimented using the Unification Workbench, a tool under development at SUNY, Albany, with the eventual goal of integrating them into application software, the NRL Protocol Analyzer and a rewrite-based induction theorem prover RRL (Rewrite Rule Laboratory) for use in the applications discussed above.This award is one of three in a collaborative research team. The three awards are CCR-0098114 (Deepak Kapur, U New Mexico), CCR-0098270 (Christopher Lynch, Clarkson U), and CCR-0098095 (Paliath Narendran, SUNY Albany).

提案#0098114Kupar，DeepakUniversity of Mexico语义统一已有效地应用于逻辑、计算机科学、人工智能和认知科学的许多子领域，其最流行的用途是解析、逻辑编程语言（例如Prolog）以及中的类型推断机制。编程语言 ML。语义统一（结合交换统一）在解决数学中的开放性问题方面发挥了关键作用（例如，McCune 在 1996 年使用定理证明器 EQP 提出了罗宾斯关于布尔代数的猜想）。最近，人们发现语义统一在密码分析、知识表示和分布式计算中也很有用。该项目将是语义统一理论研究以及语义统一算法的设计、开发和实现的延续。这项研究将受到语义统一在密码协议分析中的新应用的推动，并结合 Catherine Meadows 在 NRL（海军研究实验室）协议分析器、知识表示和描述逻辑、归纳定理证明和过程代数方面的工作。统一算法将首先使用 Unification Workbench 进行开发和实验，Unification Workbench 是纽约州立大学奥尔巴尼分校正在开发的一个工具，最终目标是将它们集成到应用软件、NRL 协议分析器和基于重写的归纳定理证明器 RRL（重写规则实验室），用于上述应用。该奖项是合作研究团队的三个奖项之一。这三个奖项分别是 CCR-0098114（Deepak Kapur，新墨西哥大学）、CCR-0098270（Christopher Lynch，克拉克森大学）和 CCR-0098095（Paliath Narendran，纽约州立大学奥尔巴尼分校）。