Theories with associative and commutative (AC) operators, such as arithmetic, process algebras, boolean algebras, sets,… are ubiqnitous in software and hardware verification. These AC operators are difficult to handle by automatic deduction since they generate complex proofs. In this paper, we present new techniques for combining induction and AC reasoning, in a rewrite-based theorem prover. The resulting system has proved to be quite successful for verification tasks. Thanks to its careful rewriting strategy, it needs less interaction on typical verification problems than well known tools like NQTHM, LP or PVS. We also believe that our approach can easily be integrated as an efficient tactic in other proof systems.
CITATION STYLE
Berregeb, N., Bouhoula, A., & Rusinowitch, M. (1996). Automated verification by induction with associative-commutative operators. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1102, pp. 220–231). Springer Verlag. https://doi.org/10.1007/3-540-61474-5_71
Mendeley helps you to discover research relevant for your work.