Gabbay, D; Ohlbach, HJ
(South African Computer Society (SAICSIT), 1992)
An algorithm is presented which eliminates second-order quantifiers over predicate variables in formulae of type 3Pi , ...,Pn 1/; where 1/J is an arbitrary formula of first-order predicate logic. The resulting formula is ...