Collaborative Research on Semantic Unification and its Applications

Clarkson University, Potsdam NY

Investigators

Abstract

Propoal #0098270 Clarkson University Lynch, Christopher Semantic 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).