# Accession Number:

## ADP006611

# Title:

## High Performance Simplification-Based Automated Deduction,

# Descriptive Note:

# Corporate Author:

## STATE UNIV OF NEW YORK AT STONY BROOK DEPT OF COMPUTER SCIENCE

# Personal Author(s):

# Report Date:

## 1992-03-01

# Pagination or Media Count:

## 15.0

# Abstract:

Equational logic is one of the most important domains of research in computer science. Specifications of types of data structures and assertions about the behaviour of programs are naturally written in equational form. Programs made of equations are called equational programs and appear in functional programming, logic programming and in most combinations of high level programming paradigms 19, 23. First order logic can be expressed, equationally 20. This formulation makes it possible to express logic programming equationally and to employ the computation model of equational languages in logic programming 7. Set theory can also be expressed equationally 33, enabling one to reason about query languages and optimization in data bases 11. Such a wide range of applications, not to mention the traditional applications to algebra, makes automated deduction in equational logic an important subject of research. However, the seemingly insurmountable search space caused by the symmetry and replacement properties of the equality predicate had been a serious obstacle which baffled researchers in automated deduction for several decades. It is not until very recently that methods capable of effectively reason with equations have been designed and successfully applied to an interesting range of challenging problems. These methods are based on the term rewriting approach to equational reasoning, which was started in 24.

# Descriptors:

# Subject Categories:

- Computer Programming and Software