eCommons

 

Determining Logical Dependency in a Decision Procedure for Equality

Other Titles

Abstract

Several existing program verification and automated prooff systems make use of similar decision procedures for equality ([Krafft 1978], [Nelson and Oppen 1977] and [Downey, Sethi and Tarjan 1980]). The general method used by these algorithms has been named congruence closure. Given two expressions on uninterpreted function symbols, a congruence closure algorithm determines whether the expressions can be deduced to be equal from a set of previously asserted equalities. The existing congruence closure algorithms do not provide any indication of which previously asserted equalities were required in the deduction. In this paper, we describe an extension to one version of congruence closure. When two expressions are equal, the new algorithm can provide a certificate of their equality: a list of prevviously asserted equalities from which the queried equality can be deduced. This list is minimal, in the sense that if any equality iss removed from the list, the queried equality can no longer be deduced. The running time to produce the certificate is almost-linear in the size of the list.

Journal / Series

Volume & Issue

Description

Sponsorship

Date Issued

1981-04

Publisher

Cornell University

Keywords

computer science; technical report

Location

Effective Date

Expiration Date

Sector

Employer

Union

Union Local

NAICS

Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)

References

Link(s) to Reference(s)

Previously Published As

http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR81-458

Government Document

ISBN

ISMN

ISSN

Other Identifiers

Rights

Rights URI

Types

technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record