Accession Number : ADP006611

Title :   High Performance Simplification-Based Automated Deduction,

Corporate Author : STATE UNIV OF NEW YORK AT STONY BROOK DEPT OF COMPUTER SCIENCE

Personal Author(s) : Bonacina, Maria Paola ; Hsiang, Jieh

Report Date : MAR 1992

Pagination or Media Count : 15

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 :   *COMPUTER LOGIC, *HIGH LEVEL LANGUAGES, *COMPUTER PROGRAMMING, ALGEBRA, COMPUTATIONS, COMPUTERS, DATA BASES, EQUATIONS, FORMULATIONS, LOGIC, MODELS, OPTIMIZATION, SET THEORY, SPECIFICATIONS, STRUCTURES, SYMMETRY, THEORY.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE