Regular Strategies as Proof Tactics for CIRC

Dorel Lucanu; Grigore Roşu; Gheorghe Grigoraş

doi:10.1016/j.entcs.2008.03.055

Regular Strategies as Proof Tactics for CIRC

Dorel Lucanu, Grigore Roşu, Gheorghe Grigoraş

Research output: Contribution to journal › Article › peer-review

Abstract

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.

Original language	English (US)
Pages (from-to)	83-98
Number of pages	16
Journal	Electronic Notes in Theoretical Computer Science
Volume	204
Issue number	C
DOIs	https://doi.org/10.1016/j.entcs.2008.03.055
State	Published - Apr 4 2008

Keywords

Behavioral equivalence
circular coinduction
proof tactics
regular strategies

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Online availability

10.1016/j.entcs.2008.03.055

Library availability

Discover UIUC Full Text

Cite this

@article{bf5c53770cf647a0969dee18dce26436,

title = "Regular Strategies as Proof Tactics for CIRC",

abstract = "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.",

keywords = "Behavioral equivalence, circular coinduction, proof tactics, regular strategies",

author = "Dorel Lucanu and Grigore Ro{\c s}u and Gheorghe Grigora{\c s}",

note = "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",

year = "2008",

month = apr,

day = "4",

doi = "10.1016/j.entcs.2008.03.055",

language = "English (US)",

volume = "204",

pages = "83--98",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

number = "C",

}

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 - 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 -

Regular Strategies as Proof Tactics for CIRC

Abstract

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this