Decision procedures for the propositional cases of second order logic and Z modal logic representations of a first order L-predicate nonmonotonic logic

Decision procedures for the propositional cases of two different logical representations for an LPredicate Logic generalizing Autoepistemic Logic to handle quantified variables over modal scopes are described. The first representation is Second Order Logic. The second is Z Modal Logic which extends its S5 modal laws with laws stating what is logically possible. It is suggested that certain problems are more easily solved using one representation whereas other problems axe more easily solved using the other.