Abstract

An essential element of automated deduction systems is unification algorithms which identify general substitutions and when applied to two expressions, make them identical. However, functions which are associative and commutative, such as the usual addition and multiplication functions, often arise in term rewriting systems, program verification, the theory of abstract data types and logic programming. The introduction to the associative and commutative equality axioms together with standard unification brings with it problems of termination and unreasonably large search spaces. One way around these problems is to remove the troublesome axioms from the system and to employ a unification algorithm which unifies modulo the axioms of associativity and commutativity. Unlike standard unification, the associative-commutative (AC) unification of two expressions can lead to the formation of many most general unifiers. A report is presented on a hybrid AC unification algorithm which has been implemented to run in parallel on an Intel iPSC/2

Meeting Name

13th Annual International Computer Software and Applications Conference, 1989. COMPSAC 89

Department(s)

Computer Science

Keywords and Phrases

Intel IPSC/2; Abstract Data Types; Associative-Commutative Unification Speedups; Automated Deduction Systems; Commutative Equality Axioms; Formal Logic; General Substitutions; Hybrid AC Unification Algorithm; Inference Mechanisms; Logic Programming; Multicomputer Environment; Parallel; Parallel Algorithms; Parallel Machines; Program Verification; Standard Unification; Symbol Manipulation; Term Rewriting Systems; Termination; Unreasonably Large Search Spaces

Document Type

Article - Conference proceedings

Document Version

Final Version

File Type

text

Language(s)

English

Rights

© 1989 Institute of Electrical and Electronics Engineers (IEEE), All rights reserved.

Publication Date

01 Jan 1989

Download

Full Text Link

Share

 
COinS