TY - JOUR
T1 - Regular Strategies as Proof Tactics for CIRC
AU - Lucanu, Dorel
AU - Roşu, Grigore
AU - Grigoraş, Gheorghe
N1 - 1 Partially supported by CEEX grant 47/2005 and CNCSIS grant 1162/2007. 2 Partially supported by NSF grants CCF-0448501 and CNS-0509321. 3 Email: [email protected] 4 Email: [email protected] 5 Email: [email protected]
PY - 2008/4/4
Y1 - 2008/4/4
N2 - CIRC is an automated circular coinductive prover implemented as an extension of Maude. The main engine of CIRC consists of a set of rewriting rules implementing the circularity principle. The power of the prover can be increased by adding new capabilities implemented also by rewriting rules. In this paper we prove the correctness of the coinductive prover and show how rewriting strategies, expressed as regular expressions, can be used for specifying proof tactics for CIRC. We illustrate the strength of the method by defining a proof tactic combining the circular coinduction with a particular form of simplification for proving the equivalence of context-free processes.
AB - CIRC is an automated circular coinductive prover implemented as an extension of Maude. The main engine of CIRC consists of a set of rewriting rules implementing the circularity principle. The power of the prover can be increased by adding new capabilities implemented also by rewriting rules. In this paper we prove the correctness of the coinductive prover and show how rewriting strategies, expressed as regular expressions, can be used for specifying proof tactics for CIRC. We illustrate the strength of the method by defining a proof tactic combining the circular coinduction with a particular form of simplification for proving the equivalence of context-free processes.
KW - Behavioral equivalence
KW - circular coinduction
KW - proof tactics
KW - regular strategies
UR - http://www.scopus.com/inward/record.url?scp=41649085561&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=41649085561&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2008.03.055
DO - 10.1016/j.entcs.2008.03.055
M3 - Article
AN - SCOPUS:41649085561
SN - 1571-0661
VL - 204
SP - 83
EP - 98
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
IS - C
ER -