Jancar's formal system for deciding bisimulation of first-order grammars and its non-soundness

TL;DR

This paper demonstrates a flaw in a formal system designed to decide bisimulation for non-deterministic first-order grammars, showing that its proof can lead to incorrect conclusions about semantic equivalence.

Contribution

It identifies and analyzes a critical flaw in the soundness proof of a formal system for bisimulation of first-order grammars, challenging previous assumptions.

Findings

Constructed a counterexample proof within the system

Showed the proof's conclusion is semantically false

Identified a flaw in the system's soundness proof

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.