Automata for the tex2html_wrap_inline19 -calculus and Related Results

David Janin
Igor Walukiewicz

May 1995


The propositional tex2html_wrap_inline19 -calculus as introduced by Kozen in [TCS 27] is considered. The notion of disjunctive formula is defined and it is shown that every formula is semantically equivalent to a disjunctive formula. For these formulas many difficulties encountered in the general case may be avoided. For instance, satisfiability checking is linear for disjunctive formulas. This kind of formula gives rise to a new notion of finite automaton which characterizes the expressive power of the tex2html_wrap_inline19 -calculus over all transition systems.

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.