Jancar's formal system for deciding bisimulation of first-order grammars and its non-soundness
Formal Languages and Automata Theory
2011-01-27 v1 Logic in Computer Science
Abstract
We construct an example of proof within the main formal system from arXiv:1010.4760v3, which is intended to capture the bisimulation equivalence for non-deterministic first-order grammars, and show that its conclusion is semantically false. We then locate and analyze the flawed argument in the soundness (meta)-proof of the above reference.
Keywords
Cite
@article{arxiv.1101.5046,
title = {Jancar's formal system for deciding bisimulation of first-order grammars and its non-soundness},
author = {Géraud Sénizergues},
journal= {arXiv preprint arXiv:1101.5046},
year = {2011}
}
Comments
12 pages, 9 figures