some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

SPECIAL ISSUES

   Recent

   In Progress

   Archive

   Proposal

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

SPECIAL ISSUE:
Selected Papers of the Confrence 'Tools and Algorithms for the Construction and Analysis of Systems "TACAS" 2011'



Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation

©Sylvain Conchon, LRI-UPS
©Evelyne Contejean, LRI-CNRS
©Mohamed Iguernelala, LRI-UPS

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 AC-completion 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.

Publication date: September 14, 2012

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-8(3:16)2012

Hit Counts: 5639

Creative Commons