This Article 
 Bibliographic References 
 Add to: 
Efficient On-Line Proofs of Equalities and Inequalities of Formulas
January 1980 (vol. 29 no. 1)
pp. 28-32
H. Samet, Department of Computer Science, University of Maryland
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
H. Samet, "Efficient On-Line Proofs of Equalities and Inequalities of Formulas," IEEE Transactions on Computers, vol. 29, no. 1, pp. 28-32, Jan. 1980, doi:10.1109/TC.1980.1675453
Usage of this product signifies your acceptance of the Terms of Use.