Regular strategies as proof tactics for CIRC

Dorel Lucanu, Grigore Rosu, Gheorghe Grigoraş

Research output: Contribution to journalConference article

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 languageEnglish (US)
Pages (from-to)69-83
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
StatePublished - Dec 1 2007
Event7th 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 - Paris, France
Duration: Jun 25 2007Jun 25 2007

Fingerprint

Rewriting
Engines
Coinduction
Maude
Regular Expressions
Simplification
Correctness
Engine
Equivalence
Strategy

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Regular strategies as proof tactics for CIRC. / Lucanu, Dorel; Rosu, Grigore; Grigoraş, Gheorghe.

In: Electronic Notes in Theoretical Computer Science, 01.12.2007, p. 69-83.

Research output: Contribution to journalConference article

@article{1e703475a24141d68d9917f56da19f43,
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.",
author = "Dorel Lucanu and Grigore Rosu and Gheorghe Grigoraş",
year = "2007",
month = "12",
day = "1",
language = "English (US)",
pages = "69--83",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

T1 - Regular strategies as proof tactics for CIRC

AU - Lucanu, Dorel

AU - Rosu, Grigore

AU - Grigoraş, Gheorghe

PY - 2007/12/1

Y1 - 2007/12/1

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

SP - 69

EP - 83

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -