Regular Strategies as Proof Tactics for CIRC | Zendy

Dorel Lucanu | Zendy; Grigore Roşu | Zendy; Gheorghe Grigoraş | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Regular Strategies as Proof Tactics for CIRC

Author(s) -

Dorel Lucanu,

Grigore Roşu,

Gheorghe Grigoraş

Publication year - 2008

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2008.03.055

Subject(s) - coinduction , rewriting , gas meter prover , correctness , equivalence (formal languages) , programming language , computer science , extension (predicate logic) , automated theorem proving , proof assistant , context (archaeology) , mathematics , algorithm , discrete mathematics , calculus (dental) , algebra over a field , mathematical proof , pure mathematics , paleontology , geometry , biology , medicine , dentistry

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research