Monadic second-order logic
In mathematical logic, monadic second order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets.[1] It is particularly important in the logic of graphs, because of Courcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over certain types of graphs.
Existential monadic second-order logic (EMSO) is the fragment of MSO in which all quantifiers over sets must be existential quantifiers, outside of any other part of the formula. The first-order quantifiers are not restricted. By analogy to Fagin's theorem, according to which existential (non-monadic) second-order logic captures precisely the descriptive complexity of the complexity class NP, the class of problems that may be expressed in existential monadic second-order logic has been called monadic NP. The restriction to monadic logic makes it possible to prove separations in this logic that remain unproven for non-monadic second-order logic; for instance, testing the connectivity of graphs belongs to monadic co-NP (the complement of monadic NP) but not to monadic NP itself.[2][3]
References
- ^ Courcelle, Bruno; Engelfriet, Joost (2012-01-01). Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Cambridge University Press. ISBN 978-0521898331. Retrieved 2016-09-15.
- ^ Fagin, Ronald (1975), "Monadic generalized spectra", Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 21: 89–96, MR 0371623.
- ^ Fagin, R.; Stockmeyer, L.; Vardi, M. Y. (1993), "On monadic NP vs. monadic co-NP", Proceedings of the Eighth Annual Structure in Complexity Theory Conference, Institute of Electrical and Electronics Engineers, doi:10.1109/sct.1993.336544.