Issue No. 01 - January (1980 vol. 29)

ISSN: 0018-9340

pp: 28-32

H. Samet , Department of Computer Science, University of Maryland

ABSTRACT

An algorithm is presented for proving equivalence and inequivalence of instances of formulas involving constant terms. It is based on the construction of an equality data base in the form of a grammar. The algorithm differes from other approaches to the problem by being an on-line algorithm. Equality between two formulas can be proved in time proportional to the number of constant and function symbols appearing within them. An algorithm is also given for updating the equality data base. It has a worse case running time which is proportional to the square of the number of different formulas previously encountered.

INDEX TERMS

theorem proving, Equality, code optimization, hashing, on-line algorithms, program verification, symbolic execution

CITATION

H. Samet, "Efficient On-Line Proofs of Equalities and Inequalities of Formulas",

*IEEE Transactions on Computers*, vol. 29, no. , pp. 28-32, January 1980, doi:10.1109/TC.1980.1675453