Regular Strategies as Proof Tactics for CIRC

Dorel Lucanu, Grigore Roşu, Gheorghe Grigoraş

Research output: Contribution to journalArticle

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)83-98
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Volume204
Issue numberC
DOIs
StatePublished - Apr 4 2008

Keywords

  • Behavioral equivalence
  • circular coinduction
  • proof tactics
  • regular strategies

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Regular Strategies as Proof Tactics for CIRC'. Together they form a unique fingerprint.

  • Cite this