Quantifier elimination in second order predicate logic

dc.contributor.author	Gabbay, D
dc.contributor.author	Ohlbach, HJ
dc.date.accessioned	2018-05-23T09:53:26Z
dc.date.available	2018-05-23T09:53:26Z
dc.date.issued	1992
dc.identifier.citation	Gabbay D & Ohlbach HJ (1992) Quantifier elimination in second order predicate logic. The South African Computer Journal, Number 7, 1992	en
dc.identifier.issn	2313-7835
dc.identifier.uri	http://hdl.handle.net/10500/24024
dc.description.abstract	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 equivalent to the original formula - if the algorithm termiantes. The algorithm can for example be applied to do interpolation, to eliminate the second-order quantifiers in circumscription, to compute semantic properties corresponding to Hilbert axioms in non classical logics and to compute model theoretic semantics for new logics.	en
dc.language.iso	en	en
dc.publisher	South African Computer Society (SAICSIT)	en
dc.subject	Quantifier elimination	en
dc.subject	Second-order predicate logic	en
dc.subject	Circumscription	en
dc.subject	Interpolation	en
dc.title	Quantifier elimination in second order predicate logic	en
dc.type	Article	en