Canonized Rewriting and Ground AC Completion Modulo Shostak Theories

Sylvain Conchon 1, 2 Evelyne Contejean 1, 2 Mohamed Iguernelala 1, 2
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-00777663
Contributor : Claude Marché <>
Submitted on : Thursday, January 17, 2013 - 5:20:41 PM
Last modification on : Thursday, April 5, 2018 - 12:30:08 PM

File

conchon11tacas.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00777663, version 1

Collections

Citation

Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. TACAS - Tools and Algorithms for the Construction and Analysis of Systems, 2011, Saarbrücken, Germany. ⟨hal-00777663⟩

Share

Metrics

Record views

602

Files downloads

291