Quantifier elimination in second order predicate logic
Loading...
Authors
Gabbay, D
Ohlbach, HJ
Issue Date
1992
Type
Article
Language
en
Keywords
Quantifier elimination , Second-order predicate logic , Circumscription , Interpolation
Alternative Title
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.
Description
Citation
Gabbay D & Ohlbach HJ (1992) Quantifier elimination in second order predicate logic. The South African Computer Journal, Number 7, 1992
Publisher
South African Computer Society (SAICSIT)
License
Journal
Volume
Issue
PubMed ID
DOI
ISSN
2313-7835