Using Proofs by Coinduction to Find "Traditional" Proofs

In the specific situation of formal reasoning concerned with “regular expression equivalence” we address instances of more general questions such as: how can coinductive argumentation be formalised logically and be applied effectively, as well as how is it linked to traditional forms of proof. For statements expressing that two regular expressions are language equivalent, we demonstrate that proofs by coinduction can be formulated in a proof system based on equational logic, where effective proof-search is possible. And we describe a proof-theoretic method for translating derivations in this proof system into a “traditional” axiom system: namely, into a “reverse form” of the axiomatisation of “regular expression equivalence” due to Salomaa. Hereby we obtain a coinductive completeness proof for the traditional proof system.

• Type: Conference
• Year: 2005
• Where: CALCO
• Authors: Clemens Grabmayer
• Keywords: CALCO 2005, Coinductive Completeness Proof, Regular Expression, Regular Expression Equivalence