Abstract
In this paper, we develop the basic theory of disimulations, a type of relation between two automata which witnesses equivalence. We show that many standard constructions in the theory of automata such as determinization, minimization, inaccessible state removal, et al., are instances of disimilar automata. Then, using disimulations, we define an "algebraic" proof system for the equational theory of Kleene algebra in which a proof essentially consists of a sequence of matrices encoding automata and disimulations between them. We show that this proof system is complete for the equational theory of Kleene algebra, and that proofs in this system can be constructed by a PSPACE transducer. © 2008 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Worthington, J. (2008). Automatic proof generation in kleene algebra. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4988 LNCS, pp. 382–396). Springer Verlag. https://doi.org/10.1007/978-3-540-78913-0_28
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
