Abstract
AC-completion efficiently handles equality modulo associative and commutative function symbols. When the input is ground, the procedure terminates and provides a decision algorithm for the word problem. In this paper, we present a modular extension of ground ACcompletion for deciding formulas in the combination of the theory of equality with user-defined AC symbols, uninterpreted symbols and an arbitrary signature disjoint Shostak theory X. Our algorithm, called AC(X), is obtained by augmenting in a modular way ground AC-completion with the canonizer and solver present for the theory X. This integration rests on canonized rewriting, a new relation reminiscent to normalized rewriting, which integrates canonizers in rewriting steps. AC(X) is proved sound, complete and terminating, and is implemented to extend the core of the Alt-Ergo theorem prover.
Work partially supported by the French ANR project ANR-08-005 Decert.
Chapter PDF
Similar content being viewed by others
Keywords
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Bachmair, L., Dershowitz, N., Hsiang, J.: Orderings for equational proofs. In: Proc. 1st LICS, Cambridge, Mass., pp. 346–357 (June 1986)
Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. Journal of Automated Reasoning 31(2), 129–168 (2003)
Conchon, S., Contejean, E., Iguernelala, M.: Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. Research Report 1538, LRI (December 2010)
Contejean, E.: A certified AC matching algorithm. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 70–84. Springer, Heidelberg (2004)
Dershowitz, N.: Orderings for term rewriting systems. Theoretical Computer Science 17(3), 279–301 (1982)
Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 243–320. North-Holland, Amsterdam (1990)
Conchon, S., Contejean, E., Bobot, F., Lescuyer, S., Iguernelala, M.: The Alt-Ergo theorem prover, http://alt-ergo.lri.fr
Hullot, J.-M.: Associative commutative pattern matching. In: Proc. 6th IJCAI, Tokyo, vol. I, pp. 406–412 (August 1979)
Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM Journal on Computing 15(4) (November 1986)
Kapur, D.: Shostak’s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232. Springer, Heidelberg (1997)
Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)
Krstić, S., Conchon, S.: Canonization for disjoint unions of theories. Information and Computation 199(1-2), 87–106 (2005)
Lankford, D.S.: Canonical inference. Memo ATP-32, University of Texas at Austin (March 1975)
Lankford, D.S., Ballantyne, A.M.: Decision procedures for simple equational theories with permutative axioms: Complete sets of permutative reductions. Memo ATP-37, University of Texas, Austin, Texas, USA (August 1977)
Marché, C.: On ground AC-completion. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488. Springer, Heidelberg (1991)
Marché, C.: Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation 21(3), 253–288 (1996)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. on Programming, Languages and Systems 1(2), 245–257 (1979)
Nieuwenhuis, R., Rubio, A.: A precedence-based total AC-compatible ordering. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690. Springer, Heidelberg (1993)
Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. J. ACM 28(2), 233–264 (1981)
Shostak, R.E.: Deciding combinations of theories. J. ACM 31, 1–12 (1984)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Conchon, S., Contejean, E., Iguernelala, M. (2011). Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. In: Abdulla, P.A., Leino, K.R.M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2011. Lecture Notes in Computer Science, vol 6605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19835-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-19835-9_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19834-2
Online ISBN: 978-3-642-19835-9
eBook Packages: Computer ScienceComputer Science (R0)