“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.

Second-order logic allows quantification over predicates. However, MSO is the fragment in which second-order quantification is limited to monadic predicates (predicates having a single argument). This is often described as quantification over "sets" because monadic predicates are equivalent in expressive power to sets (the set of elements for which the predicate is true).

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, in the logic of graphs, testing whether a graph is disconnected belongs to monadic NP, as the test can be represented by a formula that describes the existence of a proper subset of vertices with no edges connecting them to the rest of the graph; however, the complementary problem, testing whether a graph is connected, does not belong to monadic NP.^[2]^[3] The existence of an analogous pair of complementary problems, only one of which has an existential second-order formula (without the restriction to monadic formulas) is equivalent to the inequality of NP and coNP, an open question in computational complexity.

The monadic second order theory of the infinite complete binary tree, called S2S, is decidable. As a consequence of this result, the following theories are decidable:

For each of these theories (S2S, S1S, wS2S, wS1S), the complexity of the decision problem is nonelementary.

References

1. ^{{cite book|first1=Bruno|last1=Courcelle|author1-link=Bruno Courcelle|first2=Joost|last2=Engelfriet| title=Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach| publisher=Cambridge University Press|date=2012-01-01|isbn=978-0521898331|url=http://dl.acm.org/citation.cfm?id=2414243|accessdate=2016-09-15}}
2. ^{{citation | last = Fagin | first = Ronald | author1-link = Ronald Fagin | journal = Zeitschrift für Mathematische Logik und Grundlagen der Mathematik | mr = 0371623 | pages = 89–96 | title = Monadic generalized spectra | volume = 21 | year = 1975}}.
3. ^{{citation | last1 = Fagin | first1 = R. | author1-link = Ronald Fagin | last2 = Stockmeyer | first2 = L. | author2-link = Larry Stockmeyer | last3 = Vardi | first3 = M. Y. | author3-link = Moshe Vardi | contribution = On monadic NP vs. monadic co-NP | doi = 10.1109/sct.1993.336544 | publisher = Institute of Electrical and Electronics Engineers | title = Proceedings of the Eighth Annual Structure in Complexity Theory Conference | year = 1993}}.