Abstract:
The propositional  -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 -calculus over all
transition systems.
Available as PostScript, PDF,
DVI.
|