TY - JOUR
T1 - Regular strategies as proof tactics for CIRC
AU - Lucanu, Dorel
AU - Roşu, Grigore
AU - Grigoraş, Gheorghe
N1 - Funding Information:
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: dlucanu@info.uaic.ro 4 Email: grosu@cs.uiuc.edu 5 Email: grigoras@info.uaic.ro
PY - 2007
Y1 - 2007
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.
UR - http://www.scopus.com/inward/record.url?scp=84890257199&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84890257199&partnerID=8YFLogxK
M3 - Conference article
AN - SCOPUS:84890257199
SN - 1571-0661
SP - 69
EP - 83
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
T2 - 7th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2007, as part of the 4th Federated Conference on Rewriting, Deduction, and Programming, RDP 2007
Y2 - 25 June 2007 through 25 June 2007
ER -