Abstract
Proofs of equalities may be built from assumptions using proof rules for reflexivity, symmetry, and transitivity. Reflexivity is an axiom proving x=x for any x; symmetry is a 1-premise rule taking a proof of x=y and returning a proof of y=x; and transitivity is a 2-premise rule taking proofs of x=y and y=z, and returning a proof of x=z. Define an equivalence relation to hold between proofs iff they prove a theorem in common. The main theoretical result of the paper is that if all assumptions are independent, this equivalence relation is axiomatized by the standard axioms of group theory: reflexivity is the unit of the group, symmetry is the inverse, and transitivity is the multiplication. Using a standard completion of the group axioms, we obtain a rewrite system which puts equality proofs into canonical form. Proofs in this canonical form use the fewest possible assumptions, and a proof can be canonized in linear time using a simple strategy. This result is applied to obtain a simple extension of the union-find algorithm for ground equational reasoning which produces minimal proofs. The time complexity of the original union-find operations is preserved, and minimal proofs are produced in worst-case time \(O(n^{\textit{log}_2 3})\), where n is the number of expressions being equated. As a second application, the approach is used to achieve significant performance improvements for the CVC cooperating decision procedure.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Barrett, C., Dill, D., Stump, A.: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 236. Springer, Heidelberg (2002)
Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)
Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Cormen, T., Leiserson, C., Rivest, R.: Introduction to Algorithms. MIT Press, Cambridge (1992)
de Moura, L., Rueß, H., Shankar, N.: Justifying Equality. In: Ranise, S., Tinelli, C. (eds.) 2nd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (2004)
Filliâtre, J., Owre, S., Rueß, H., Shankar, N.: ICS: integrated canonizer and solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 246. Springer, Heidelberg (2001)
Knuth, D., Bendix, P.: SimpleWord Problems in Universal Algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)
Lahiri, S., Bryant, R., Goel, A., Talupur, M.: Revisiting Positive Equality. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 1–15. Springer, Heidelberg (2004)
Nelson, G., Oppen, D.: Fast decision procedures based on congruence closure. Journal of the Association for Computing Machinery 27(2), 356–364 (1980)
Nieuwenhuis, R., Oliveras, A.: Union-Find and Congruence Closure Algorithms that Produce Proofs. In: Ranise, S., Tinelli, C. (eds.) 2nd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (2004) (short paper)
Nieuwenhuis, R., Oliveras, A.: Proof-producing Congruence Closure. In: Giesl, J. (ed.) 16th International Conference on Rewriting Techniques and Applications (2005) (under review)
Pnueli, A., Rodeh, Y., Shtrichman, O., Siegel, M.: Deciding Equality Formulas by Small Domains Instantiations. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 455–469. Springer, Heidelberg (1999)
Ruess, H., Shankar, N.: Deconstructing Shostak. In: 16th IEEE Symposium on Logic in Computer Science (2001)
Shostak, R.: Deciding combinations of theories. Journal of the Association for Computing Machinery 31(1), 1–12 (1984)
Stump, A.: Checking Validities and Proofs with CVC and flea. PhD thesis, Stanford University (2002), available from http://www.cs.wustl.edu/~stump/
Stump, A., Barrett, C., Dill, D.: CVC: a Cooperating Validity Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 500. Springer, Heidelberg (2002)
Velev, M., Bryant, R.: Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 37–53. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stump, A., Tan, LY. (2005). The Algebra of Equality Proofs. In: Giesl, J. (eds) Term Rewriting and Applications. RTA 2005. Lecture Notes in Computer Science, vol 3467. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32033-3_34
Download citation
DOI: https://doi.org/10.1007/978-3-540-32033-3_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25596-3
Online ISBN: 978-3-540-32033-3
eBook Packages: Computer ScienceComputer Science (R0)