Search

• < Previous
• 1
• Next >

Deciding Kleene Algebras in Coq

We present a reflexive tactic for deciding the equational theory of Kleene algebras in the Coq proof assistant. This tactic relies on a careful implementation of efficient finite automata algorithms, so that it solves casual equations instantaneously and properly scales to larger expressions. The&nbsp;[&hellip;]